1  /-
  2  Copyright (c) 2017 Johannes Hölzl. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Johannes Hölzl, Mario Carneiro, Jeremy Avigad
  5  -/
  6  
  7  import order.filter
src         └──────────┘
  8  
  9  /-!
 10  # Basic theory of topological spaces.
 11  
 12  The main definition is the type class `topological space α` which endows a type `α` with a topology.
 13  Then `set α` gets predicates `is_open`, `is_closed` and functions `interior`, `closure` and
 14  `frontier`. Each point `x` of `α` gets a neighborhood filter `𝓝 x`.
 15  
 16  This file also defines locally finite families of subsets of `α`.
 17  
 18  For topological spaces `α` and `β`, a function `f : α → β` and a point `a : α`,
 19  `continuous_at f a` means `f` is continuous at `a`, and global continuity is
 20  `continuous f`. There is also a version of continuity `pcontinuous` for
 21  partially defined functions.
 22  
 23  ## Implementation notes
 24  
 25  Topology in mathlib heavily uses filters (even more than in Bourbaki). See explanations in
 26  `docs/theories/topology.md`.
 27  
 28  ## References
 29  
 30  *  [N. Bourbaki, *General Topology*][bourbaki1966]
 31  *  [I. M. James, *Topologies and Uniformities*][james1999]
 32  
 33  ## Tags
 34  
 35  topological space, interior, closure, frontier, neighborhood, continuity, continuous function
 36  -/
 37  
 38  open set filter lattice classical
 39  open_locale classical
 40  
 41  universes u v w
 42  
 43  /-- A topology on `α`. -/
 44  structure topological_space (α : Type u) :=
id                                    └──┘
typ                                   └──┘
 45  (is_open       : set α → Prop)
id                    └─┘  
src                   └─┘
typ                   └─┘  
 46  (is_open_univ   : is_open univ)
id                     └─────┘ └──┘
src                            └──┘
typ                    └─────┘ └──┘
 47  (is_open_inter  : ∀s t, is_open s → is_open t → is_open (s ∩ t))
id                         └─────┘    └─────┘    └─────┘    
src                                                             
typ                        └─────┘    └─────┘    └─────┘    
 48  (is_open_sUnion : ∀s, (∀t∈s, is_open t) → is_open (⋃₀ s))
id                             └─────┘     └─────┘  └┘ 
src                                                    └┘
typ                            └─────┘     └─────┘  └┘ 
 49  
 50  attribute [class] topological_space
id                     └───────────────┘
src                    └───────────────┘
typ                    └───────────────┘
doc                    └───────────────┘
 51  
 52  section topological_space
 53  
 54  variables {α : Type u} {β : Type v} {ι : Sort w} {a : α} {s s₁ s₂ : set α} {p p₁ p₂ : α → Prop}
id                                                                      └─┘
src                                                                      └─┘
typ                                                                     └─┘
 55  
 56  @[ext]
doc    └─┘
 57  lemma topological_space_eq : ∀ {f g : topological_space α}, f.is_open = g.is_open → f = g
id                                        └───────────────┘    └──────┘  └──────┘     
src                                        └───────────────┘      └──────┘   └──────┘     
typ                                       └───────────────┘    └──────┘  └──────┘     
doc                                        └───────────────┘
 58  | ⟨a, _, _, _⟩ ⟨b, _, _, _⟩ rfl := rfl
id                               └─┘    └─┘
src                              └─┘    └─┘
typ                              └─┘    └─┘
 59  
 60  section
 61  variables [t : topological_space α]
id                  └───────────────┘
src                 └───────────────┘
typ                 └───────────────┘
doc                 └───────────────┘
 62  include t
 63  
 64  /-- `is_open s` means that `s` is open in the ambient topological space on `α` -/
 65  def is_open (s : set α) : Prop := topological_space.is_open t s
id                    └─┘             └───────────────────────┘  
src                   └─┘              └───────────────────────┘
typ                   └─┘             └───────────────────────┘  
 66  
 67  @[simp]
doc    └──┘
 68  lemma is_open_univ : is_open (univ : set α) := topological_space.is_open_univ t
id                        └─────┘  └──┘   └─┘      └────────────────────────────┘ 
src                       └─────┘  └──┘   └─┘       └────────────────────────────┘
typ                       └─────┘  └──┘   └─┘      └────────────────────────────┘ 
doc                       └─────┘
 69  
 70  lemma is_open_inter (h₁ : is_open s₁) (h₂ : is_open s₂) : is_open (s₁ ∩ s₂) :=
id                             └─────┘ └┘        └─────┘ └┘    └─────┘  └┘  └┘
src                            └─────┘           └─────┘       └─────┘     
typ                            └─────┘ └┘        └─────┘ └┘    └─────┘  └┘  └┘
doc                            └─────┘           └─────┘       └─────┘
 71  topological_space.is_open_inter t s₁ s₂ h₁ h₂
id   └─────────────────────────────┘  └┘ └┘ └┘ └┘
src  └─────────────────────────────┘
typ  └─────────────────────────────┘  └┘ └┘ └┘ └┘
 72  
 73  lemma is_open_sUnion {s : set (set α)} (h : ∀t ∈ s, is_open t) : is_open (⋃₀ s) :=
id                             └─┘  └─┘               └─────┘     └─────┘  └┘ 
src                            └─┘  └─┘                  └─────┘      └─────┘  └┘
typ                            └─┘  └─┘               └─────┘     └─────┘  └┘ 
doc                                                      └─────┘      └─────┘
 74  topological_space.is_open_sUnion t s h
id   └──────────────────────────────┘   
src  └──────────────────────────────┘
typ  └──────────────────────────────┘   
 75  
 76  end
 77  
 78  lemma is_open_fold {s : set α} {t : topological_space α} : t.is_open s = @is_open α t s :=
id                           └─┘        └───────────────┘     └──────┘    └─────┘   
src                          └─┘         └───────────────┘       └──────┘     └─────┘
typ                          └─┘        └───────────────┘     └──────┘    └─────┘   
doc                                      └───────────────┘                     └─────┘
 79  rfl
id   └─┘
src  └─┘
typ  └─┘
 80  
 81  variables [topological_space α]
id              └───────────────┘
src             └───────────────┘
typ             └───────────────┘
doc             └───────────────┘
 82  
 83  lemma is_open_Union {f : ι → set α} (h : ∀i, is_open (f i)) : is_open (⋃i, f i) :=
id                               └─┘           └─────┘        └─────┘    
src                               └─┘             └─────┘          └─────┘   
typ                              └─┘           └─────┘        └─────┘    
doc                                               └─────┘          └─────┘   
 84  is_open_sUnion $ by rintro _ ⟨i, rfl⟩; exact h i
id   └────────────┘                                
src  └────────────┘      └───────────────┘  └────┘  
typ  └────────────┘      └───────────────┘  └────┘
doc                      └───────────────┘  └────┘  
txt                      └───────────────┘  └────┘  
par                      └───────────────┘  └────┘  
pid                            └─────────┘         
st                      └─────────────────────────────
 85  
src  
typ  
doc  
txt  
par  
pid  
st   
 86  lemma is_open_bUnion {s : set β} {f : β → set α} (h : ∀i∈s, is_open (f i)) :
id                             └─┘           └─┘            └─────┘   
src                            └─┘             └─┘               └─────┘
typ                            └─┘           └─┘            └─────┘   
doc                                                              └─────┘
 87    is_open (⋃i∈s, f i) :=
id     └─────┘     
src    └─────┘     
typ    └─────┘     
doc    └─────┘     
 88  is_open_Union $ assume i, is_open_Union $ assume hi, h i hi
id   └───────────┘            └───────────┘          └┘    └┘
src  └───────────┘             └───────────┘
typ  └───────────┘            └───────────┘          └┘    └┘
 89  
 90  lemma is_open_union (h₁ : is_open s₁) (h₂ : is_open s₂) : is_open (s₁ ∪ s₂) :=
id                             └─────┘ └┘        └─────┘ └┘    └─────┘  └┘  └┘
src                            └─────┘           └─────┘       └─────┘     
typ                            └─────┘ └┘        └─────┘ └┘    └─────┘  └┘  └┘
doc                            └─────┘           └─────┘       └─────┘
 91  by rw union_eq_Union; exact is_open_Union (bool.forall_bool.2 ⟨h₂, h₁⟩)
id         └────────────┘        └───────────┘  └──────────────┘    └┘  └┘
src     └─┘└────────────┘  └────┘└───────────┘ └──────────────┘└─┘   └┘  └──
typ     └─┘└────────────┘  └────┘└───────────┘ └──────────────┘└─┘ └┘└┘└┘└──
doc     └─┘                └────┘                              └─┘   └┘  └──
txt     └─┘                └────┘                              └─┘   └┘  └──
par     └─┘                └────┘                              └─┘   └┘  └──
pid                                                          └─┘   └┘  └┘
st     └─────────────────────────────────────────────────────────────────────
 92  
src  
typ  
doc  
txt  
par  
pid  
st   
 93  @[simp] lemma is_open_empty : is_open (∅ : set α) :=
id                                 └─────┘     └─┘ 
src                                └─────┘     └─┘
typ                                └─────┘     └─┘ 
doc    └──┘                        └─────┘
 94  by rw ← sUnion_empty; exact is_open_sUnion (assume a, false.elim)
id           └──────────┘        └────────────┘            └────────┘
src     └───┘└──────────┘  └────┘└────────────┘       └──┘└────────┘└─
typ     └───┘└──────────┘  └────┘└────────────┘       └──┘└────────┘└─
doc     └───┘              └────┘                     └──┘          └─
txt     └───┘              └────┘                     └──┘          └─
par     └───┘              └────┘                     └──┘          └─
pid       └─┘                                        └──┘          
st     └───────────────────────────────────────────────────────────────
 95  
src  
typ  
doc  
txt  
par  
pid  
st   
 96  lemma is_open_sInter {s : set (set α)} (hs : finite s) : (∀t ∈ s, is_open t) → is_open (⋂₀ s) :=
id                             └─┘  └─┘          └────┘            └─────┘     └─────┘  └┘ 
src                            └─┘  └─┘           └────┘               └─────┘      └─────┘  └┘
typ                            └─┘  └─┘          └────┘            └─────┘     └─────┘  └┘ 
doc                                               └────┘               └─────┘      └─────┘  └┘
 97  finite.induction_on hs (λ _, by rw sInter_empty; exact is_open_univ) $
id   └─────────────────┘ └┘            └──────────┘        └──────────┘
src  └─────────────────┘             └─┘└──────────┘  └────┘└──────────┘
typ  └─────────────────┘ └┘         └─┘└──────────┘  └────┘└──────────┘
doc                                  └─┘              └────┘
txt                                  └─┘              └────┘
par                                  └─┘              └────┘
pid                                                       
st                                  └──────────────────────────────────┘
 98  λ a s has hs ih h, by rw sInter_insert; exact
id       └─┘ └┘ └┘         └───────────┘
src                        └─┘└───────────┘  └────┘
typ      └─┘ └┘ └┘      └─┘└───────────┘  └────┘
doc                        └─┘               └────┘
txt                        └─┘               └────┘
par                        └─┘               └────┘
pid                                              
st                        └────────────────────────
 99  is_open_inter (h _ $ mem_insert _ _) (ih $ λ t, h t ∘ mem_insert_of_mem _)
id   └───────────┘        └────────┘       └┘            └───────────────┘
src  └───────────┘  └─┘ └────────┘└────┘     └──┘  └───────────────┘└───
typ  └───────────┘  └─┘ └────────┘└────┘ └┘  └──┘ └───────────────┘└───
doc                 └─┘           └────┘     └──┘                    └───
txt                 └─┘           └────┘     └──┘                    └───
par                 └─┘           └────┘     └──┘                    └───
pid                 └─┘           └────┘     └──┘                    └─┘
st   ───────────────────────────────────────────────────────────────────────────
100  
src  
typ  
doc  
txt  
par  
pid  
st   
101  lemma is_open_bInter {s : set β} {f : β → set α} (hs : finite s) :
id                             └─┘           └─┘         └────┘ 
src                            └─┘             └─┘          └────┘
typ                            └─┘           └─┘         └────┘ 
doc                                                         └────┘
102    (∀i∈s, is_open (f i)) → is_open (⋂i∈s, f i) :=
id          └─────┘        └─────┘     
src           └─────┘          └─────┘     
typ         └─────┘        └─────┘     
doc           └─────┘          └─────┘     
103  finite.induction_on hs
id   └─────────────────┘ └┘
src  └─────────────────┘
typ  └─────────────────┘ └┘
104    (λ _, by rw bInter_empty; exact is_open_univ)
id                └──────────┘        └──────────┘
src             └─┘└──────────┘  └────┘└──────────┘
typ            └─┘└──────────┘  └────┘└──────────┘
doc             └─┘              └────┘
txt             └─┘              └────┘
par             └─┘              └────┘
pid                                  
st             └──────────────────────────────────┘
105    (λ a s has hs ih h, by rw bInter_insert; exact
id          └─┘ └┘ └┘         └───────────┘
src                           └─┘└───────────┘  └─────
typ         └─┘ └┘ └┘      └─┘└───────────┘  └─────
doc                           └─┘               └─────
txt                           └─┘               └─────
par                           └─┘               └─────
pid                                                 
st                          └────────────────────────
106      is_open_inter (h a (mem_insert _ _)) (ih (λ i hi, h i (mem_insert_of_mem _ hi))))
id       └───────────┘      └────────┘        └┘              └───────────────┘
src  ───┘└───────────┘    └────────┘└─────┘     └─────┘   └───────────────┘└─┘  └─┘
typ  ───┘└───────────┘   └────────┘└─────┘ └┘  └─────┘  └───────────────┘└─┘  └─┘
doc  ───┘                           └─────┘     └─────┘                    └─┘  └─┘
txt  ───┘                           └─────┘     └─────┘                    └─┘  └─┘
par  ───┘                           └─────┘     └─────┘                    └─┘  └─┘
pid  ───┘                           └─────┘     └─────┘                    └─┘  └─┘
st   ───────────────────────────────────────────────────────────────────────────────────┘
107  
108  lemma is_open_Inter [fintype β] {s : β → set α}
id                        └─────┘           └─┘ 
src                       └─────┘             └─┘
typ                       └─────┘           └─┘ 
doc                       └─────┘
109    (h : ∀ i, is_open (s i)) : is_open (⋂ i, s i) :=
id              └─────┘        └─────┘     
src              └─────┘          └─────┘    
typ             └─────┘        └─────┘     
doc              └─────┘          └─────┘    
110  suffices is_open (⋂ (i : β) (hi : i ∈ @univ β), s i), by simpa,
id            └─────┘                   └──┘    
src           └─────┘                     └──┘             └───┘
typ           └─────┘                   └──┘          └───┘
doc           └─────┘                                       └───┘
txt                                                           └───┘
par                                                           └───┘
st                                                           └────┘
111  is_open_bInter finite_univ (λ i _, h i)
id   └────────────┘ └─────────┘        
src  └────────────┘ └─────────┘
typ  └────────────┘ └─────────┘        
112  
113  lemma is_open_Inter_prop {p : Prop} {s : p → set α}
id                                               └─┘ 
src                                               └─┘
typ                                              └─┘ 
114    (h : ∀ h : p, is_open (s h)) : is_open (Inter s) :=
id                  └─────┘        └─────┘  └───┘ 
src                  └─────┘          └─────┘  └───┘
typ                 └─────┘        └─────┘  └───┘ 
doc                  └─────┘          └─────┘  └───┘
115  by by_cases p; simp *
id               
src     └───────┘   └──────
typ     └───────┘  └──────
doc     └───────┘   └──────
txt     └───────┘   └──────
par     └───────┘   └──────
pid                    
st     └───────────────────
116  
src  
typ  
doc  
txt  
par  
pid  
st   
117  lemma is_open_const {p : Prop} : is_open {a : α | p} :=
id                                    └─────┘        
src                                   └─────┘ 
typ                                   └─────┘        
doc                                   └─────┘
118  by_cases
id   └──────┘
src  └──────┘
typ  └──────┘
119    (assume : p, begin simp only [this]; exact is_open_univ end)
id                                  └──┘         └──────────┘
src                       └─────────┘      └────┘└──────────┘
typ                      └─────────┘└──┘  └────┘└──────────┘
doc                       └─────────┘      └────┘            
txt                       └─────────┘      └────┘            
par                       └─────────┘      └────┘            
pid                           └──┘└┘                       
st                  └─────────────────────────────────────────┘└─┘
120    (assume : ¬ p, begin simp only [this]; exact is_open_empty end)
id                                   └──┘         └───────────┘
src                        └─────────┘      └────┘└───────────┘
typ                       └─────────┘└──┘  └────┘└───────────┘
doc                         └─────────┘      └────┘             
txt                         └─────────┘      └────┘             
par                         └─────────┘      └────┘             
pid                             └──┘└┘                        
st                    └──────────────────────────────────────────┘└─┘
121  
122  lemma is_open_and : is_open {a | p₁ a} → is_open {a | p₂ a} → is_open {a | p₁ a ∧ p₂ a} :=
id                       └─────┘    └┘     └─────┘    └┘     └─────┘    └┘   └┘ 
src                      └─────┘             └─────┘             └─────┘          
typ                      └─────┘    └┘     └─────┘    └┘     └─────┘    └┘   └┘ 
doc                      └─────┘              └─────┘              └─────┘
123  is_open_inter
id   └───────────┘
src  └───────────┘
typ  └───────────┘
124  
125  /-- A set is closed if its complement is open -/
126  def is_closed (s : set α) : Prop := is_open (-s)
id                      └─┘             └─────┘  
src                     └─┘              └─────┘  
typ                     └─┘             └─────┘  
doc                                      └─────┘
127  
128  @[simp] lemma is_closed_empty : is_closed (∅ : set α) :=
id                                   └───────┘     └─┘ 
src                                  └───────┘     └─┘
typ                                  └───────┘     └─┘ 
doc    └──┘                          └───────┘
129  by unfold is_closed; rw compl_empty; exact is_open_univ
id                           └─────────┘        └──────────┘
src     └──────────────┘  └─┘└─────────┘  └────┘└──────────┘
typ     └──────────────┘  └─┘└─────────┘  └────┘└──────────┘
doc     └──────────────┘  └─┘             └────┘            
txt     └──────────────┘  └─┘             └────┘            
par     └──────────────┘  └─┘             └────┘            
pid           └────────┘                                  
st     └────────────────────┘└─────────┘└────────────────────
130  
src  
typ  
doc  
txt  
par  
pid  
st   
131  @[simp] lemma is_closed_univ : is_closed (univ : set α) :=
id                                  └───────┘  └──┘   └─┘ 
src                                 └───────┘  └──┘   └─┘
typ                                 └───────┘  └──┘   └─┘ 
doc    └──┘                         └───────┘
132  by unfold is_closed; rw compl_univ; exact is_open_empty
id                           └────────┘        └───────────┘
src     └──────────────┘  └─┘└────────┘  └────┘└───────────┘
typ     └──────────────┘  └─┘└────────┘  └────┘└───────────┘
doc     └──────────────┘  └─┘            └────┘             
txt     └──────────────┘  └─┘            └────┘             
par     └──────────────┘  └─┘            └────┘             
pid           └────────┘                                  
st     └────────────────────┘└────────┘└─────────────────────
133  
src  
typ  
doc  
txt  
par  
pid  
st   
134  lemma is_closed_union : is_closed s₁ → is_closed s₂ → is_closed (s₁ ∪ s₂) :=
id                           └───────┘ └┘   └───────┘ └┘   └───────┘  └┘  └┘
src                          └───────┘      └───────┘      └───────┘     
typ                          └───────┘ └┘   └───────┘ └┘   └───────┘  └┘  └┘
doc                          └───────┘      └───────┘      └───────┘
135  λ h₁ h₂, by unfold is_closed; rw compl_union; exact is_open_inter h₁ h₂
id     └┘ └┘                          └─────────┘        └───────────┘ └┘ └┘
src              └──────────────┘  └─┘└─────────┘  └────┘└───────────┘    
typ    └┘ └┘     └──────────────┘  └─┘└─────────┘  └────┘└───────────┘└┘└┘
doc              └──────────────┘  └─┘             └────┘                 
txt              └──────────────┘  └─┘             └────┘                 
par              └──────────────┘  └─┘             └────┘                 
pid                    └────────┘                                       
st              └────────────────────┘└─────────┘└───────────────────────────
136  
src  
typ  
doc  
txt  
par  
pid  
st   
137  lemma is_closed_sInter {s : set (set α)} : (∀t ∈ s, is_closed t) → is_closed (⋂₀ s) :=
id                               └─┘  └─┘             └───────┘     └───────┘  └┘ 
src                              └─┘  └─┘                └───────┘      └───────┘  └┘
typ                              └─┘  └─┘             └───────┘     └───────┘  └┘ 
doc                                                      └───────┘      └───────┘  └┘
138  by simp only [is_closed, compl_sInter, sUnion_image]; exact assume h, is_open_Union $ assume t, is_open_Union $ assume ht, h t ht
id                 └───────┘  └──────────┘  └──────────┘                                             └───────────┘
src     └─────────┘└───────┘└┘└──────────┘└┘└──────────┘  └────┘      └──┘                    └──┘└───────────┘       └───┘    
typ     └─────────┘└───────┘└┘└──────────┘└┘└──────────┘  └────┘      └──┘                    └──┘└───────────┘       └───┘    
doc     └─────────┘└───────┘└┘            └┘              └────┘      └──┘                    └──┘                    └───┘    
txt     └─────────┘         └┘            └┘              └────┘      └──┘                    └──┘                    └───┘    
par     └─────────┘         └┘            └┘              └────┘      └──┘                    └──┘                    └───┘    
pid         └──┘└┘         └┘            └┘                         └──┘                    └──┘                    └───┘    
st     └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
139  
src  
typ  
doc  
txt  
par  
pid  
st   
140  lemma is_closed_Inter {f : ι → set α} (h : ∀i, is_closed (f i)) : is_closed (⋂i, f i ) :=
id                                 └─┘           └───────┘        └───────┘    
src                                 └─┘             └───────┘          └───────┘   
typ                                └─┘           └───────┘        └───────┘    
doc                                                 └───────┘          └───────┘   
141  is_closed_sInter $ assume t ⟨i, (heq : f i = t)⟩, heq ▸ h i
id   └──────────────┘                                
src  └──────────────┘                                    
typ  └──────────────┘                                
142  
143  @[simp] lemma is_open_compl_iff {s : set α} : is_open (-s) ↔ is_closed s := iff.rfl
id                                        └─┘     └─────┘     └───────┘     └─────┘
src                                       └─┘      └─────┘      └───────┘      └─────┘
typ                                       └─┘     └─────┘     └───────┘     └─────┘
doc    └──┘                                        └─────┘        └───────┘
144  
145  @[simp] lemma is_closed_compl_iff {s : set α} : is_closed (-s) ↔ is_open s :=
id                                          └─┘     └───────┘     └─────┘ 
src                                         └─┘      └───────┘      └─────┘
typ                                         └─┘     └───────┘     └─────┘ 
doc    └──┘                                          └───────┘        └─────┘
146  by rw [←is_open_compl_iff, compl_compl]
id           └───────────────┘  └─────────┘
src     └───┘└───────────────┘└┘└─────────┘└─
typ     └───┘└───────────────┘└┘└─────────┘└─
doc     └───┘                 └┘           └─
txt     └───┘                 └┘           └─
par     └───┘                 └┘           └─
pid       └─┘                 └┘           
st     └─────────────────────┘└───────────┘
147  
src  
typ  
doc  
txt  
par  
pid  
st   
148  lemma is_open_diff {s t : set α} (h₁ : is_open s) (h₂ : is_closed t) : is_open (s \ t) :=
id                             └─┘         └─────┘         └───────┘     └─────┘    
src                            └─┘          └─────┘          └───────┘      └─────┘    
typ                            └─┘         └─────┘         └───────┘     └─────┘    
doc                                         └─────┘          └───────┘      └─────┘
149  is_open_inter h₁ $ is_open_compl_iff.mpr h₂
id   └───────────┘ └┘   └───────────────┘└──┘ └┘
src  └───────────┘      └───────────────┘└──┘
typ  └───────────┘ └┘   └───────────────┘└──┘ └┘
150  
151  lemma is_closed_inter (h₁ : is_closed s₁) (h₂ : is_closed s₂) : is_closed (s₁ ∩ s₂) :=
id                               └───────┘ └┘        └───────┘ └┘    └───────┘  └┘  └┘
src                              └───────┘           └───────┘       └───────┘     
typ                              └───────┘ └┘        └───────┘ └┘    └───────┘  └┘  └┘
doc                              └───────┘           └───────┘       └───────┘
152  by rw [is_closed, compl_inter]; exact is_open_union h₁ h₂
id          └───────┘  └─────────┘         └───────────┘ └┘ └┘
src     └──┘└───────┘└┘└─────────┘  └────┘└───────────┘    
typ     └──┘└───────┘└┘└─────────┘  └────┘└───────────┘└┘└┘
doc     └──┘└───────┘└┘             └────┘                 
txt     └──┘         └┘             └────┘                 
par     └──┘         └┘             └────┘                 
pid       └┘         └┘                                   
st     └────────────┘└───────────┘└───────────────────────────
153  
src  
typ  
doc  
txt  
par  
pid  
st   
154  lemma is_closed_bUnion {s : set β} {f : β → set α} (hs : finite s) :
id                               └─┘           └─┘         └────┘ 
src                              └─┘             └─┘          └────┘
typ                              └─┘           └─┘         └────┘ 
doc                                                           └────┘
155    (∀i∈s, is_closed (f i)) → is_closed (⋃i∈s, f i) :=
id          └───────┘        └───────┘     
src           └───────┘          └───────┘     
typ         └───────┘        └───────┘     
doc           └───────┘          └───────┘     
156  finite.induction_on hs
id   └─────────────────┘ └┘
src  └─────────────────┘
typ  └─────────────────┘ └┘
157    (λ _, by rw bUnion_empty; exact is_closed_empty)
id                └──────────┘        └─────────────┘
src             └─┘└──────────┘  └────┘└─────────────┘
typ            └─┘└──────────┘  └────┘└─────────────┘
doc             └─┘              └────┘
txt             └─┘              └────┘
par             └─┘              └────┘
pid                                  
st             └─────────────────────────────────────┘
158    (λ a s has hs ih h, by rw bUnion_insert; exact
id          └─┘ └┘ └┘         └───────────┘
src                           └─┘└───────────┘  └─────
typ         └─┘ └┘ └┘      └─┘└───────────┘  └─────
doc                           └─┘               └─────
txt                           └─┘               └─────
par                           └─┘               └─────
pid                                                 
st                           └────────────────────────
159      is_closed_union (h a (mem_insert _ _)) (ih (λ i hi, h i (mem_insert_of_mem _ hi))))
id       └─────────────┘      └────────┘        └┘              └───────────────┘
src  ───┘└─────────────┘    └────────┘└─────┘     └─────┘   └───────────────┘└─┘  └─┘
typ  ───┘└─────────────┘   └────────┘└─────┘ └┘  └─────┘  └───────────────┘└─┘  └─┘
doc  ───┘                             └─────┘     └─────┘                    └─┘  └─┘
txt  ───┘                             └─────┘     └─────┘                    └─┘  └─┘
par  ───┘                             └─────┘     └─────┘                    └─┘  └─┘
pid  ───┘                             └─────┘     └─────┘                    └─┘  └─┘
st   ─────────────────────────────────────────────────────────────────────────────────────┘
160  
161  lemma is_closed_Union [fintype β] {s : β → set α}
id                          └─────┘           └─┘ 
src                         └─────┘             └─┘
typ                         └─────┘           └─┘ 
doc                         └─────┘
162    (h : ∀ i, is_closed (s i)) : is_closed (Union s) :=
id              └───────┘        └───────┘  └───┘ 
src              └───────┘          └───────┘  └───┘
typ             └───────┘        └───────┘  └───┘ 
doc              └───────┘          └───────┘  └───┘
163  suffices is_closed (⋃ (i : β) (hi : i ∈ @univ β), s i),
id            └───────┘                   └──┘    
src           └───────┘                     └──┘   
typ           └───────┘                   └──┘    
doc           └───────┘                             
164    by convert this; simp [set.ext_iff],
id                └──┘        └─────────┘
src       └──────┘      └────┘└─────────┘
typ       └──────┘└──┘  └────┘└─────────┘
doc       └──────┘      └────┘           
txt       └──────┘      └────┘           
par       └──────┘      └────┘           
pid                                   
st       └───────────────────────────────┘
165  is_closed_bUnion finite_univ (λ i _, h i)
id   └──────────────┘ └─────────┘        
src  └──────────────┘ └─────────┘
typ  └──────────────┘ └─────────┘        
166  
167  lemma is_closed_Union_prop {p : Prop} {s : p → set α}
id                                                 └─┘ 
src                                                 └─┘
typ                                                └─┘ 
168    (h : ∀ h : p, is_closed (s h)) : is_closed (Union s) :=
id                  └───────┘        └───────┘  └───┘ 
src                  └───────┘          └───────┘  └───┘
typ                 └───────┘        └───────┘  └───┘ 
doc                  └───────┘          └───────┘  └───┘
169  by by_cases p; simp *
id               
src     └───────┘   └──────
typ     └───────┘  └──────
doc     └───────┘   └──────
txt     └───────┘   └──────
par     └───────┘   └──────
pid                    
st     └───────────────────
170  
src  
typ  
doc  
txt  
par  
pid  
st   
171  lemma is_closed_imp {p q : α → Prop} (hp : is_open {x | p x})
id                                             └─────┘     
src                                             └─────┘ 
typ                                            └─────┘     
doc                                             └─────┘
172    (hq : is_closed {x | q x}) : is_closed {x | p x → q x} :=
id           └───────┘          └───────┘         
src          └───────┘             └───────┘ 
typ          └───────┘          └───────┘         
doc          └───────┘              └───────┘
173  have {x | p x → q x} = (- {x | p x}) ∪ {x | q x}, from set.ext $ λ x, imp_iff_not_or,
id                                         └─────┘       └────────────┘
src                                                   └─────┘        └────────────┘
typ                                        └─────┘       └────────────┘
174  by rw [this]; exact is_closed_union (is_closed_compl_iff.mpr hp) hq
id          └──┘         └─────────────┘  └─────────────────────┘ └┘  └┘
src     └──┘      └────┘└─────────────┘ └─────────────────────┘  └┘  
typ     └──┘└──┘  └────┘└─────────────┘ └─────────────────────┘└┘└┘└┘
doc     └──┘      └────┘                                         └┘  
txt     └──┘      └────┘                                         └┘  
par     └──┘      └────┘                                         └┘  
pid       └┘                                                    └┘  
st     └───────┘└───────────────────────────────────────────────────────
175  
src  
typ  
doc  
txt  
par  
pid  
st   
176  lemma is_open_neg : is_closed {a | p a} → is_open {a | ¬ p a} :=
id                       └───────┘         └─────┘      
src                      └───────┘            └─────┘     
typ                      └───────┘         └─────┘      
doc                      └───────┘             └─────┘
177  is_open_compl_iff.mpr
id   └───────────────┘└──┘
src  └───────────────┘└──┘
typ  └───────────────┘└──┘
178  
179  /-- The interior of a set `s` is the largest open subset of `s`. -/
180  def interior (s : set α) : set α := ⋃₀ {t | is_open t ∧ t ⊆ s}
id                     └─┘     └─┘     └┘    └─────┘     
src                    └─┘      └─┘      └┘     └─────┘      
typ                    └─┘     └─┘     └┘    └─────┘     
doc                                              └─────┘
181  
182  lemma mem_interior {s : set α} {x : α} :
id                           └─┘        
src                          └─┘
typ                          └─┘        
183    x ∈ interior s ↔ ∃ t ⊆ s, is_open t ∧ x ∈ t :=
id       └──────┘        └─────┘     
src       └──────┘           └─────┘      
typ      └──────┘        └─────┘     
doc        └──────┘              └─────┘
184  by simp only [interior, mem_set_of_eq, exists_prop, and_assoc, and.left_comm]
id                 └──────┘  └───────────┘  └─────────┘  └───────┘  └───────────┘
src     └─────────┘└──────┘└┘└───────────┘└┘└─────────┘└┘└───────┘└┘└───────────┘└─
typ     └─────────┘└──────┘└┘└───────────┘└┘└─────────┘└┘└───────┘└┘└───────────┘└─
doc     └─────────┘└──────┘└┘             └┘           └┘         └┘             └─
txt     └─────────┘        └┘             └┘           └┘         └┘             └─
par     └─────────┘        └┘             └┘           └┘         └┘             └─
pid         └──┘└┘        └┘             └┘           └┘         └┘             
st     └───────────────────────────────────────────────────────────────────────────
185  
src  
typ  
doc  
txt  
par  
pid  
st   
186  @[simp] lemma is_open_interior {s : set α} : is_open (interior s) :=
id                                       └─┘     └─────┘  └──────┘ 
src                                      └─┘      └─────┘  └──────┘
typ                                      └─┘     └─────┘  └──────┘ 
doc    └──┘                                       └─────┘  └──────┘
187  is_open_sUnion $ assume t ⟨h₁, h₂⟩, h₁
id   └────────────┘           └┘
src  └────────────┘
typ  └────────────┘           └┘
188  
189  lemma interior_subset {s : set α} : interior s ⊆ s :=
id                              └─┘     └──────┘   
src                             └─┘      └──────┘   
typ                             └─┘     └──────┘   
doc                                      └──────┘
190  sUnion_subset $ assume t ⟨h₁, h₂⟩, h₂
id   └───────────┘               └┘
src  └───────────┘
typ  └───────────┘               └┘
191  
192  lemma interior_maximal {s t : set α} (h₁ : t ⊆ s) (h₂ : is_open t) : t ⊆ interior s :=
id                                 └─┘                   └─────┘       └──────┘ 
src                                └─┘                      └─────┘         └──────┘
typ                                └─┘                   └─────┘       └──────┘ 
doc                                                          └─────┘          └──────┘
193  subset_sUnion_of_mem ⟨h₂, h₁⟩
id   └──────────────────┘  └┘  └┘
src  └──────────────────┘
typ  └──────────────────┘  └┘  └┘
194  
195  lemma interior_eq_of_open {s : set α} (h : is_open s) : interior s = s :=
id                                  └─┘        └─────┘     └──────┘   
src                                 └─┘         └─────┘      └──────┘   
typ                                 └─┘        └─────┘     └──────┘   
doc                                             └─────┘      └──────┘
196  subset.antisymm interior_subset (interior_maximal (subset.refl s) h)
id   └─────────────┘ └─────────────┘  └──────────────┘  └─────────┘   
src  └─────────────┘ └─────────────┘  └──────────────┘  └─────────┘
typ  └─────────────┘ └─────────────┘  └──────────────┘  └─────────┘   
197  
198  lemma interior_eq_iff_open {s : set α} : interior s = s ↔ is_open s :=
id                                   └─┘     └──────┘     └─────┘ 
src                                  └─┘      └──────┘       └─────┘
typ                                  └─┘     └──────┘     └─────┘ 
doc                                           └──────┘         └─────┘
199  ⟨assume h, h ▸ is_open_interior, interior_eq_of_open⟩
id               └──────────────┘  └─────────────────┘
src                └──────────────┘  └─────────────────┘
typ              └──────────────┘  └─────────────────┘
200  
201  lemma subset_interior_iff_open {s : set α} : s ⊆ interior s ↔ is_open s :=
id                                       └─┘       └──────┘   └─────┘ 
src                                      └─┘         └──────┘    └─────┘
typ                                      └─┘       └──────┘   └─────┘ 
doc                                                   └──────┘     └─────┘
202  by simp only [interior_eq_iff_open.symm, subset.antisymm_iff, interior_subset, true_and]
id                                            └─────────────────┘  └─────────────┘  └──────┘
src     └─────────┘                         └┘└─────────────────┘└┘└─────────────┘└┘└──────┘└─
typ     └─────────┘└───────────────────────┘└┘└─────────────────┘└┘└─────────────┘└┘└──────┘└─
doc     └─────────┘                         └┘                   └┘               └┘        └─
txt     └─────────┘                         └┘                   └┘               └┘        └─
par     └─────────┘                         └┘                   └┘               └┘        └─
pid         └──┘└┘                         └┘                   └┘               └┘        
st     └──────────────────────────────────────────────────────────────────────────────────────
203  
src  
typ  
doc  
txt  
par  
pid  
st   
204  lemma subset_interior_iff_subset_of_open {s t : set α} (h₁ : is_open s) :
id                                                   └─┘         └─────┘ 
src                                                  └─┘          └─────┘
typ                                                  └─┘         └─────┘ 
doc                                                               └─────┘
205    s ⊆ interior t ↔ s ⊆ t :=
id       └──────┘     
src       └──────┘      
typ      └──────┘     
doc        └──────┘
206  ⟨assume h, subset.trans h interior_subset, assume h₂, interior_maximal h₂ h₁⟩
id             └──────────┘  └─────────────┘         └┘  └──────────────┘ └┘ └┘
src             └──────────┘   └─────────────┘             └──────────────┘
typ            └──────────┘  └─────────────┘         └┘  └──────────────┘ └┘ └┘
207  
208  lemma interior_mono {s t : set α} (h : s ⊆ t) : interior s ⊆ interior t :=
id                              └─┘              └──────┘   └──────┘ 
src                             └─┘                 └──────┘    └──────┘
typ                             └─┘              └──────┘   └──────┘ 
doc                                                  └──────┘     └──────┘
209  interior_maximal (subset.trans interior_subset h) is_open_interior
id   └──────────────┘  └──────────┘ └─────────────┘   └──────────────┘
src  └──────────────┘  └──────────┘ └─────────────┘    └──────────────┘
typ  └──────────────┘  └──────────┘ └─────────────┘   └──────────────┘
210  
211  @[simp] lemma interior_empty : interior (∅ : set α) = ∅ :=
id                                  └──────┘     └─┘    
src                                 └──────┘     └─┘     
typ                                 └──────┘     └─┘    
doc    └──┘                         └──────┘
212  interior_eq_of_open is_open_empty
id   └─────────────────┘ └───────────┘
src  └─────────────────┘ └───────────┘
typ  └─────────────────┘ └───────────┘
213  
214  @[simp] lemma interior_univ : interior (univ : set α) = univ :=
id                                 └──────┘  └──┘   └─┘    └──┘
src                                └──────┘  └──┘   └─┘     └──┘
typ                                └──────┘  └──┘   └─┘    └──┘
doc    └──┘                        └──────┘
215  interior_eq_of_open is_open_univ
id   └─────────────────┘ └──────────┘
src  └─────────────────┘ └──────────┘
typ  └─────────────────┘ └──────────┘
216  
217  @[simp] lemma interior_interior {s : set α} : interior (interior s) = interior s :=
id                                        └─┘     └──────┘  └──────┘    └──────┘ 
src                                       └─┘      └──────┘  └──────┘     └──────┘
typ                                       └─┘     └──────┘  └──────┘    └──────┘ 
doc    └──┘                                        └──────┘  └──────┘      └──────┘
218  interior_eq_of_open is_open_interior
id   └─────────────────┘ └──────────────┘
src  └─────────────────┘ └──────────────┘
typ  └─────────────────┘ └──────────────┘
219  
220  @[simp] lemma interior_inter {s t : set α} : interior (s ∩ t) = interior s ∩ interior t :=
id                                       └─┘     └──────┘       └──────┘   └──────┘ 
src                                      └─┘      └──────┘         └──────┘    └──────┘
typ                                      └─┘     └──────┘       └──────┘   └──────┘ 
doc    └──┘                                       └──────┘           └──────┘     └──────┘
221  subset.antisymm
id   └─────────────┘
src  └─────────────┘
typ  └─────────────┘
222    (subset_inter (interior_mono $ inter_subset_left s t) (interior_mono $ inter_subset_right s t))
id      └──────────┘  └───────────┘   └───────────────┘     └───────────┘   └────────────────┘  
src     └──────────┘  └───────────┘   └───────────────┘       └───────────┘   └────────────────┘
typ     └──────────┘  └───────────┘   └───────────────┘     └───────────┘   └────────────────┘  
223    (interior_maximal (inter_subset_inter interior_subset interior_subset) $ is_open_inter is_open_interior is_open_interior)
id      └──────────────┘  └────────────────┘ └─────────────┘ └─────────────┘    └───────────┘ └──────────────┘ └──────────────┘
src     └──────────────┘  └────────────────┘ └─────────────┘ └─────────────┘    └───────────┘ └──────────────┘ └──────────────┘
typ     └──────────────┘  └────────────────┘ └─────────────┘ └─────────────┘    └───────────┘ └──────────────┘ └──────────────┘
224  
225  lemma interior_union_is_closed_of_interior_empty {s t : set α} (h₁ : is_closed s) (h₂ : interior t = ∅) :
id                                                           └─┘         └───────┘         └──────┘   
src                                                          └─┘          └───────┘          └──────┘    
typ                                                          └─┘         └───────┘         └──────┘   
doc                                                                       └───────┘          └──────┘
226    interior (s ∪ t) = interior s :=
id     └──────┘       └──────┘ 
src    └──────┘         └──────┘
typ    └──────┘       └──────┘ 
doc    └──────┘           └──────┘
227  have interior (s ∪ t) ⊆ s, from
id        └──────┘       
src       └──────┘        
typ       └──────┘       
doc       └──────┘
228    assume x ⟨u, ⟨(hu₁ : is_open u), (hu₂ : u ⊆ s ∪ t)⟩, (hx₁ : x ∈ u)⟩,
id                       └─────┘                           
src                         └─────┘                                
typ                      └─────┘                           
doc                         └─────┘
229    classical.by_contradiction $ assume hx₂ : x ∉ s,
id     └────────────────────────┘                  
src    └────────────────────────┘                  
typ    └────────────────────────┘                  
230      have u \ s ⊆ t,
id                 
src                
typ                
231        from assume x ⟨h₁, h₂⟩, or.resolve_left (hu₂ h₁) h₂,
id                      └┘  └┘   └─────────────┘
src                                └─────────────┘
typ                     └┘  └┘   └─────────────┘
232      have u \ s ⊆ interior t,
id                 └──────┘ 
src                 └──────┘
typ                └──────┘ 
doc                   └──────┘
233        by rwa subset_interior_iff_subset_of_open (is_open_diff hu₁ h₁),
id                └────────────────────────────────┘  └──────────┘ └─┘ └┘
src           └──┘└────────────────────────────────┘ └──────────┘     
typ           └──┘└────────────────────────────────┘ └──────────┘└─┘└┘
doc           └──┘                                                    
txt           └──┘                                                    
par           └──┘                                                    
pid                                                                  
st           └───────────────────────────────────────────────────────────┘
234      have u \ s ⊆ ∅,
id                 
src                 
typ                
235        by rwa h₂ at this,
id                └┘
src           └──┘  └──────┘
typ           └──┘└┘└──────┘
doc           └──┘  └──────┘
txt           └──┘  └──────┘
par           └──┘  └──────┘
pid                └──────┘
st           └─────────────┘
236      this ⟨hx₁, hx₂⟩,
id       └──┘       └─┘
typ      └──┘       └─┘
237  subset.antisymm
id   └─────────────┘
src  └─────────────┘
typ  └─────────────┘
238    (interior_maximal this is_open_interior)
id      └──────────────┘ └──┘ └──────────────┘
src     └──────────────┘      └──────────────┘
typ     └──────────────┘ └──┘ └──────────────┘
239    (interior_mono $ subset_union_left _ _)
id      └───────────┘   └───────────────┘
src     └───────────┘   └───────────────┘
typ     └───────────┘   └───────────────┘
240  
241  lemma is_open_iff_forall_mem_open : is_open s ↔ ∀ x ∈ s, ∃ t ⊆ s, is_open t ∧ x ∈ t :=
id                                       └─────┘               └─────┘     
src                                      └─────┘                    └─────┘      
typ                                      └─────┘               └─────┘     
doc                                      └─────┘                       └─────┘
242  by rw ← subset_interior_iff_open; simp only [subset_def, mem_interior]
id           └──────────────────────┘             └────────┘  └──────────┘
src     └───┘└──────────────────────┘  └─────────┘└────────┘└┘└──────────┘└─
typ     └───┘└──────────────────────┘  └─────────┘└────────┘└┘└──────────┘└─
doc     └───┘                          └─────────┘          └┘            └─
txt     └───┘                          └─────────┘          └┘            └─
par     └───┘                          └─────────┘          └┘            └─
pid       └─┘                              └──┘└┘          └┘            
st     └────────────────────────────────────────────────────────────────────
243  
src  
typ  
doc  
txt  
par  
pid  
st   
244  /-- The closure of `s` is the smallest closed set containing `s`. -/
245  def closure (s : set α) : set α := ⋂₀ {t | is_closed t ∧ s ⊆ t}
id                    └─┘     └─┘     └┘    └───────┘     
src                   └─┘      └─┘      └┘     └───────┘      
typ                   └─┘     └─┘     └┘    └───────┘     
doc                                     └┘      └───────┘
246  
247  @[simp] lemma is_closed_closure {s : set α} : is_closed (closure s) :=
id                                        └─┘     └───────┘  └─────┘ 
src                                       └─┘      └───────┘  └─────┘
typ                                       └─┘     └───────┘  └─────┘ 
doc    └──┘                                        └───────┘  └─────┘
248  is_closed_sInter $ assume t ⟨h₁, h₂⟩, h₁
id   └──────────────┘           └┘
src  └──────────────┘
typ  └──────────────┘           └┘
249  
250  lemma subset_closure {s : set α} : s ⊆ closure s :=
id                             └─┘       └─────┘ 
src                            └─┘         └─────┘
typ                            └─┘       └─────┘ 
doc                                         └─────┘
251  subset_sInter $ assume t ⟨h₁, h₂⟩, h₂
id   └───────────┘               └┘
src  └───────────┘
typ  └───────────┘               └┘
252  
253  lemma closure_minimal {s t : set α} (h₁ : s ⊆ t) (h₂ : is_closed t) : closure s ⊆ t :=
id                                └─┘                   └───────┘     └─────┘   
src                               └─┘                      └───────┘      └─────┘   
typ                               └─┘                   └───────┘     └─────┘   
doc                                                         └───────┘      └─────┘
254  sInter_subset_of_mem ⟨h₂, h₁⟩
id   └──────────────────┘  └┘  └┘
src  └──────────────────┘
typ  └──────────────────┘  └┘  └┘
255  
256  lemma closure_eq_of_is_closed {s : set α} (h : is_closed s) : closure s = s :=
id                                      └─┘        └───────┘     └─────┘   
src                                     └─┘         └───────┘      └─────┘   
typ                                     └─┘        └───────┘     └─────┘   
doc                                                 └───────┘      └─────┘
257  subset.antisymm (closure_minimal (subset.refl s) h) subset_closure
id   └─────────────┘  └─────────────┘  └─────────┘     └────────────┘
src  └─────────────┘  └─────────────┘  └─────────┘       └────────────┘
typ  └─────────────┘  └─────────────┘  └─────────┘     └────────────┘
258  
259  lemma closure_eq_iff_is_closed {s : set α} : closure s = s ↔ is_closed s :=
id                                       └─┘     └─────┘     └───────┘ 
src                                      └─┘      └─────┘       └───────┘
typ                                      └─┘     └─────┘     └───────┘ 
doc                                               └─────┘         └───────┘
260  ⟨assume h, h ▸ is_closed_closure, closure_eq_of_is_closed⟩
id               └───────────────┘  └─────────────────────┘
src                └───────────────┘  └─────────────────────┘
typ              └───────────────┘  └─────────────────────┘
261  
262  lemma closure_subset_iff_subset_of_is_closed {s t : set α} (h₁ : is_closed t) :
id                                                       └─┘         └───────┘ 
src                                                      └─┘          └───────┘
typ                                                      └─┘         └───────┘ 
doc                                                                   └───────┘
263    closure s ⊆ t ↔ s ⊆ t :=
id     └─────┘       
src    └─────┘         
typ    └─────┘       
doc    └─────┘
264  ⟨subset.trans subset_closure, assume h, closure_minimal h h₁⟩
id    └──────────┘ └────────────┘           └─────────────┘  └┘
src   └──────────┘ └────────────┘            └─────────────┘
typ   └──────────┘ └────────────┘           └─────────────┘  └┘
265  
266  lemma closure_mono {s t : set α} (h : s ⊆ t) : closure s ⊆ closure t :=
id                             └─┘              └─────┘   └─────┘ 
src                            └─┘                 └─────┘    └─────┘
typ                            └─┘              └─────┘   └─────┘ 
doc                                                 └─────┘     └─────┘
267  closure_minimal (subset.trans h subset_closure) is_closed_closure
id   └─────────────┘  └──────────┘  └────────────┘  └───────────────┘
src  └─────────────┘  └──────────┘   └────────────┘  └───────────────┘
typ  └─────────────┘  └──────────┘  └────────────┘  └───────────────┘
268  
269  lemma monotone_closure (α : Type*) [topological_space α] : monotone (@closure α _) :=
id                                       └───────────────┘     └──────┘   └─────┘ 
src                                      └───────────────┘      └──────┘   └─────┘
typ                                      └───────────────┘     └──────┘   └─────┘ 
doc                                      └───────────────┘      └──────┘   └─────┘
270  λ _ _, closure_mono
id        └──────────┘
src         └──────────┘
typ       └──────────┘
271  
272  lemma closure_inter_subset_inter_closure (s t : set α) :
id                                                   └─┘ 
src                                                  └─┘
typ                                                  └─┘ 
273    closure (s ∩ t) ⊆ closure s ∩ closure t :=
id     └─────┘       └─────┘   └─────┘ 
src    └─────┘         └─────┘    └─────┘
typ    └─────┘       └─────┘   └─────┘ 
doc    └─────┘           └─────┘     └─────┘
274  (monotone_closure α).map_inf_le s t
id    └──────────────┘  └────────┘   
src   └──────────────┘   └────────┘
typ   └──────────────┘  └────────┘   
275  
276  lemma is_closed_of_closure_subset {s : set α} (h : closure s ⊆ s) : is_closed s :=
id                                          └─┘        └─────┘       └───────┘ 
src                                         └─┘         └─────┘         └───────┘
typ                                         └─┘        └─────┘       └───────┘ 
doc                                                     └─────┘          └───────┘
277  by rw subset.antisymm subset_closure h; exact is_closed_closure
id         └─────────────┘ └────────────┘         └───────────────┘
src     └─┘└─────────────┘└────────────┘   └────┘└───────────────┘
typ     └─┘└─────────────┘└────────────┘  └────┘└───────────────┘
doc     └─┘                                └────┘                 
txt     └─┘                                └────┘                 
par     └─┘                                └────┘                 
pid                                                             
st     └─────────────────────────────────────────────────────────────
278  
src  
typ  
doc  
txt  
par  
pid  
st   
279  @[simp] lemma closure_empty : closure (∅ : set α) = ∅ :=
id                                 └─────┘     └─┘    
src                                └─────┘     └─┘     
typ                                └─────┘     └─┘    
doc    └──┘                        └─────┘
280  closure_eq_of_is_closed is_closed_empty
id   └─────────────────────┘ └─────────────┘
src  └─────────────────────┘ └─────────────┘
typ  └─────────────────────┘ └─────────────┘
281  
282  lemma closure_empty_iff (s : set α) : closure s = ∅ ↔ s = ∅ :=
id                                └─┘     └─────┘       
src                               └─┘      └─────┘         
typ                               └─┘     └─────┘       
doc                                        └─────┘
283  ⟨subset_eq_empty subset_closure, λ h, h.symm ▸ closure_empty⟩
id    └─────────────┘ └────────────┘      └───┘  └───────────┘
src   └─────────────┘ └────────────┘        └───┘  └───────────┘
typ   └─────────────┘ └────────────┘      └───┘  └───────────┘
284  
285  @[simp] lemma closure_univ : closure (univ : set α) = univ :=
id                                └─────┘  └──┘   └─┘    └──┘
src                               └─────┘  └──┘   └─┘     └──┘
typ                               └─────┘  └──┘   └─┘    └──┘
doc    └──┘                       └─────┘
286  closure_eq_of_is_closed is_closed_univ
id   └─────────────────────┘ └────────────┘
src  └─────────────────────┘ └────────────┘
typ  └─────────────────────┘ └────────────┘
287  
288  @[simp] lemma closure_closure {s : set α} : closure (closure s) = closure s :=
id                                      └─┘     └─────┘  └─────┘    └─────┘ 
src                                     └─┘      └─────┘  └─────┘     └─────┘
typ                                     └─┘     └─────┘  └─────┘    └─────┘ 
doc    └──┘                                      └─────┘  └─────┘      └─────┘
289  closure_eq_of_is_closed is_closed_closure
id   └─────────────────────┘ └───────────────┘
src  └─────────────────────┘ └───────────────┘
typ  └─────────────────────┘ └───────────────┘
290  
291  @[simp] lemma closure_union {s t : set α} : closure (s ∪ t) = closure s ∪ closure t :=
id                                      └─┘     └─────┘       └─────┘   └─────┘ 
src                                     └─┘      └─────┘         └─────┘    └─────┘
typ                                     └─┘     └─────┘       └─────┘   └─────┘ 
doc    └──┘                                      └─────┘           └─────┘     └─────┘
292  subset.antisymm
id   └─────────────┘
src  └─────────────┘
typ  └─────────────┘
293    (closure_minimal (union_subset_union subset_closure subset_closure) $ is_closed_union is_closed_closure is_closed_closure)
id      └─────────────┘  └────────────────┘ └────────────┘ └────────────┘    └─────────────┘ └───────────────┘ └───────────────┘
src     └─────────────┘  └────────────────┘ └────────────┘ └────────────┘    └─────────────┘ └───────────────┘ └───────────────┘
typ     └─────────────┘  └────────────────┘ └────────────┘ └────────────┘    └─────────────┘ └───────────────┘ └───────────────┘
294    ((monotone_closure α).le_map_sup s t)
id       └──────────────┘  └────────┘   
src      └──────────────┘   └────────┘
typ      └──────────────┘  └────────┘   
295  
296  lemma interior_subset_closure {s : set α} : interior s ⊆ closure s :=
id                                      └─┘     └──────┘   └─────┘ 
src                                     └─┘      └──────┘    └─────┘
typ                                     └─┘     └──────┘   └─────┘ 
doc                                              └──────┘     └─────┘
297  subset.trans interior_subset subset_closure
id   └──────────┘ └─────────────┘ └────────────┘
src  └──────────┘ └─────────────┘ └────────────┘
typ  └──────────┘ └─────────────┘ └────────────┘
298  
299  lemma closure_eq_compl_interior_compl {s : set α} : closure s = - interior (- s) :=
id                                              └─┘     └─────┘    └──────┘   
src                                             └─┘      └─────┘     └──────┘  
typ                                             └─┘     └─────┘    └──────┘   
doc                                                      └─────┘       └──────┘
300  begin
st   └─────
301    unfold interior closure is_closed,
src    └───────────────────────────────┘
typ    └───────────────────────────────┘
doc    └───────────────────────────────┘
txt    └───────────────────────────────┘
par    └───────────────────────────────┘
pid          └─────────────────────────┘
st   ──────────────────────────────────┘└─
302    rw [compl_sUnion, compl_image_set_of],
id         └──────────┘  └────────────────┘
src    └──┘└──────────┘└┘└────────────────┘
typ    └──┘└──────────┘└┘└────────────────┘
doc    └──┘            └┘                  
txt    └──┘            └┘                  
par    └──┘            └┘                  
pid      └┘            └┘                  
st   ─────────────────┘└──────────────────┘└──
303    simp only [compl_subset_compl]
id                └────────────────┘
src    └─────────┘└────────────────┘└┘
typ    └─────────┘└────────────────┘└┘
doc    └─────────┘                  └┘
txt    └─────────┘                  └┘
par    └─────────┘                  └┘
pid        └──┘└┘                  
st   ────────────────────────────────┘
304  end
st   └─┘
305  
306  @[simp] lemma interior_compl {s : set α} : interior (- s) = - closure s :=
id                                     └─┘     └──────┘       └─────┘ 
src                                    └─┘      └──────┘        └─────┘
typ                                    └─┘     └──────┘       └─────┘ 
doc    └──┘                                     └──────┘           └─────┘
307  by simp [closure_eq_compl_interior_compl]
id            └─────────────────────────────┘
src     └────┘└─────────────────────────────┘└─
typ     └────┘└─────────────────────────────┘└─
doc     └────┘                               └─
txt     └────┘                               └─
par     └────┘                               └─
pid                                        
st     └───────────────────────────────────────
308  
src  
typ  
doc  
txt  
par  
pid  
st   
309  @[simp] lemma closure_compl {s : set α} : closure (- s) = - interior s :=
id                                    └─┘     └─────┘       └──────┘ 
src                                   └─┘      └─────┘        └──────┘
typ                                   └─┘     └─────┘       └──────┘ 
doc    └──┘                                    └─────┘           └──────┘
310  by simp [closure_eq_compl_interior_compl]
id            └─────────────────────────────┘
src     └────┘└─────────────────────────────┘└─
typ     └────┘└─────────────────────────────┘└─
doc     └────┘                               └─
txt     └────┘                               └─
par     └────┘                               └─
pid                                        
st     └───────────────────────────────────────
311  
src  
typ  
doc  
txt  
par  
pid  
st   
312  theorem mem_closure_iff {s : set α} {a : α} :
id                                └─┘        
src                               └─┘
typ                               └─┘        
313    a ∈ closure s ↔ ∀ o, is_open o → a ∈ o → (o ∩ s).nonempty :=
id       └─────┘       └─────┘             └──────┘
src       └─────┘         └─────┘                  └──────┘
typ      └─────┘       └─────┘             └──────┘
doc        └─────┘          └─────┘                    └──────┘
314  ⟨λ h o oo ao, classical.by_contradiction $ λ os,
id        └┘ └┘  └────────────────────────┘     └┘
src                └────────────────────────┘
typ       └┘ └┘  └────────────────────────┘     └┘
315    have s ⊆ -o, from λ x xs xo, os ⟨x, xo, xs⟩,
id                      └┘ └┘  └┘    └┘  └┘
src            
typ                     └┘ └┘  └┘    └┘  └┘
316    closure_minimal this (is_closed_compl_iff.2 oo) h ao,
id     └─────────────┘ └──┘  └─────────────────┘  └┘   └┘
src    └─────────────┘       └─────────────────┘
typ    └─────────────┘ └──┘  └─────────────────┘  └┘   └┘
317  λ H c ⟨h₁, h₂⟩, classical.by_contradiction $ λ nc,
id       └┘  └┘   └────────────────────────┘     └┘
src                  └────────────────────────┘
typ      └┘  └┘   └────────────────────────┘     └┘
318    let ⟨x, hc, hs⟩ := (H _ h₁ nc) in hc (h₂ hs)⟩
id     └─┘     └┘  └┘            └┘
typ    └─┘     └┘  └┘            └┘
319  
320  lemma dense_iff_inter_open {s : set α} :
id                                   └─┘ 
src                                  └─┘
typ                                  └─┘ 
321    closure s = univ ↔ ∀ U, is_open U → U.nonempty → (U ∩ s).nonempty :=
id     └─────┘   └──┘      └─────┘    └───────┘       └──────┘
src    └─────┘    └──┘       └─────┘      └───────┘         └──────┘
typ    └─────┘   └──┘      └─────┘    └───────┘       └──────┘
doc    └─────┘                 └─────┘      └───────┘          └──────┘
322  begin
st   └─────
323    split ; intro h,
src    └────┘  └─────┘
typ    └────┘  └─────┘
doc    └────┘  └─────┘
txt    └────┘  └─────┘
par    └────┘  └─────┘
pid                └┘
st   ────────────────┘└─
324    { rintros U U_op ⟨x, x_in⟩,
src      └──────────────────────┘
typ      └──────────────────────┘
doc      └──────────────────────┘
txt      └──────────────────────┘
par      └──────────────────────┘
pid             └───────────────┘
st   ───┘└──────────────────────┘└─
325      exact mem_closure_iff.1 (by simp only [h]) U U_op x_in },
id             └─────────────┘                      └──┘ └──┘
src      └────┘└─────────────┘└─┘   └─────────┘ └┘         
typ      └────┘└─────────────┘└─┘   └─────────┘└┘└──┘└──┘
doc      └────┘               └─┘   └─────────┘ └┘         
txt      └────┘               └─┘   └─────────┘ └┘         
par      └────┘               └─┘   └─────────┘ └┘         
pid                          └─┘   └──────────┘ └─┘         
st   ──────────────────────────────┘└────────────┘└────────────┘└┘
326    { apply eq_univ_of_forall, intro x,
id             └───────────────┘
src      └────┘└───────────────┘  └─────┘
typ      └────┘└───────────────┘  └─────┘
doc      └────┘                   └─────┘
txt      └────┘                   └─────┘
par      └────┘                   └─────┘
pid                                   └┘
st   ──────────────────────────┘└───────┘└─
327      rw mem_closure_iff,
id          └─────────────┘
src      └─┘└─────────────┘
typ      └─┘└─────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ─────────────────────┘└─
328      intros U U_op x_in,
src      └────────────────┘
typ      └────────────────┘
doc      └────────────────┘
txt      └────────────────┘
par      └────────────────┘
pid            └──────────┘
st   ─────────────────────┘└─
329      exact h U U_op ⟨_, x_in⟩ },
id               └──┘     └──┘
src      └────┘       └─┘    └┘
typ      └────┘└──┘ └─┘└──┘└┘
doc      └────┘       └─┘    └┘
txt      └────┘       └─┘    └┘
par      └────┘       └─┘    └┘
pid                  └─┘    
st   ────────────────────────────┘└──
330  end
st   ──┘
331  
332  lemma dense_of_subset_dense {s₁ s₂ : set α} (h : s₁ ⊆ s₂) (hd : closure s₁ = univ) :
id                                        └─┘        └┘  └┘        └─────┘ └┘  └──┘
src                                       └─┘                       └─────┘     └──┘
typ                                       └─┘        └┘  └┘        └─────┘ └┘  └──┘
doc                                                                  └─────┘
333    closure s₂ = univ :=
id     └─────┘ └┘  └──┘
src    └─────┘     └──┘
typ    └─────┘ └┘  └──┘
doc    └─────┘
334  by { rw [← univ_subset_iff, ← hd], exact closure_mono h }
id              └─────────────┘    └┘         └──────────┘ 
src       └────┘└─────────────┘└──┘    └────┘└──────────┘ 
typ       └────┘└─────────────┘└──┘└┘  └────┘└──────────┘
doc       └────┘               └──┘    └────┘             
txt       └────┘               └──┘    └────┘             
par       └────┘               └──┘    └────┘             
pid         └──┘               └──┘                      
st     └──────────────────────┘└────┘└──────────────────────┘└┘
335  
336  /-- The frontier of a set is the set of points between the closure and interior. -/
337  def frontier (s : set α) : set α := closure s \ interior s
id                     └─┘     └─┘     └─────┘   └──────┘ 
src                    └─┘      └─┘      └─────┘    └──────┘
typ                    └─┘     └─┘     └─────┘   └──────┘ 
doc                                      └─────┘     └──────┘
338  
339  lemma frontier_eq_closure_inter_closure {s : set α} :
id                                                └─┘ 
src                                               └─┘
typ                                               └─┘ 
340    frontier s = closure s ∩ closure (- s) :=
id     └──────┘   └─────┘   └─────┘   
src    └──────┘    └─────┘    └─────┘  
typ    └──────┘   └─────┘   └─────┘   
doc    └──────┘     └─────┘     └─────┘
341  by rw [closure_compl, frontier, diff_eq]
id          └───────────┘  └──────┘  └─────┘
src     └──┘└───────────┘└┘└──────┘└┘└─────┘└─
typ     └──┘└───────────┘└┘└──────┘└┘└─────┘└─
doc     └──┘             └┘└──────┘└┘       └─
txt     └──┘             └┘        └┘       └─
par     └──┘             └┘        └┘       └─
pid       └┘             └┘        └┘       
st     └────────────────┘└────────┘└───────┘
342  
src  
typ  
doc  
txt  
par  
pid  
st   
343  /-- The complement of a set has the same frontier as the original set. -/
344  @[simp] lemma frontier_compl (s : set α) : frontier (-s) = frontier s :=
id                                     └─┘     └──────┘     └──────┘ 
src                                    └─┘      └──────┘      └──────┘
typ                                    └─┘     └──────┘     └──────┘ 
doc    └──┘                                     └──────┘        └──────┘
345  by simp only [frontier_eq_closure_inter_closure, lattice.neg_neg, inter_comm]
id                 └───────────────────────────────┘  └─────────────┘  └────────┘
src     └─────────┘└───────────────────────────────┘└┘└─────────────┘└┘└────────┘└─
typ     └─────────┘└───────────────────────────────┘└┘└─────────────┘└┘└────────┘└─
doc     └─────────┘                                 └┘               └┘          └─
txt     └─────────┘                                 └┘               └┘          └─
par     └─────────┘                                 └┘               └┘          └─
pid         └──┘└┘                                 └┘               └┘          
st     └───────────────────────────────────────────────────────────────────────────
346  
src  
typ  
doc  
txt  
par  
pid  
st   
347  lemma frontier_inter_subset (s t : set α) :
id                                      └─┘ 
src                                     └─┘
typ                                     └─┘ 
348    frontier (s ∩ t) ⊆ (frontier s ∩ closure t) ∪ (closure s ∩ frontier t) :=
id     └──────┘        └──────┘   └─────┘     └─────┘   └──────┘ 
src    └──────┘          └──────┘    └─────┘      └─────┘    └──────┘
typ    └──────┘        └──────┘   └─────┘     └─────┘   └──────┘ 
doc    └──────┘            └──────┘     └─────┘       └─────┘     └──────┘
349  begin
st   └─────
350    simp only [frontier_eq_closure_inter_closure, compl_inter, closure_union],
id                └───────────────────────────────┘  └─────────┘  └───────────┘
src    └─────────┘└───────────────────────────────┘└┘└─────────┘└┘└───────────┘
typ    └─────────┘└───────────────────────────────┘└┘└─────────┘└┘└───────────┘
doc    └─────────┘                                 └┘           └┘             
txt    └─────────┘                                 └┘           └┘             
par    └─────────┘                                 └┘           └┘             
pid        └──┘└┘                                 └┘           └┘             
st   ──────────────────────────────────────────────────────────────────────────┘└─
351    convert inter_subset_inter_left _ (closure_inter_subset_inter_closure s t),
id             └─────────────────────┘    └────────────────────────────────┘  
src    └──────┘└─────────────────────┘└─┘ └────────────────────────────────┘  
typ    └──────┘└─────────────────────┘└─┘ └────────────────────────────────┘
doc    └──────┘                       └─┘                                     
txt    └──────┘                       └─┘                                     
par    └──────┘                       └─┘                                     
pid                                  └─┘                                     
st   ───────────────────────────────────────────────────────────────────────────┘└─
352    simp only [inter_distrib_left, inter_distrib_right, inter_assoc],
id                └────────────────┘  └─────────────────┘  └─────────┘
src    └─────────┘└────────────────┘└┘└─────────────────┘└┘└─────────┘
typ    └─────────┘└────────────────┘└┘└─────────────────┘└┘└─────────┘
doc    └─────────┘                  └┘                   └┘           
txt    └─────────┘                  └┘                   └┘           
par    └─────────┘                  └┘                   └┘           
pid        └──┘└┘                  └┘                   └┘           
st   ─────────────────────────────────────────────────────────────────┘└─
353    congr' 2,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid          
st   ─────────┘└─
354    apply inter_comm
id           └────────┘
src    └────┘└────────┘
typ    └────┘└────────┘
doc    └────┘          
txt    └────┘          
par    └────┘          
pid                   
st   ──────────────────┘
355  end
st   └─┘
356  
357  lemma frontier_union_subset (s t : set α) :
id                                      └─┘ 
src                                     └─┘
typ                                     └─┘ 
358    frontier (s ∪ t) ⊆ (frontier s ∩ closure (-t)) ∪ (closure (-s) ∩ frontier t) :=
id     └──────┘        └──────┘   └─────┘       └─────┘     └──────┘ 
src    └──────┘          └──────┘    └─────┘        └─────┘      └──────┘
typ    └──────┘        └──────┘   └─────┘       └─────┘     └──────┘ 
doc    └──────┘            └──────┘     └─────┘          └─────┘        └──────┘
359  by simpa only [frontier_compl, (compl_union _ _).symm]
id                  └────────────┘   └─────────┘
src     └──────────┘└────────────┘└┘ └─────────┘└───────────
typ     └──────────┘└────────────┘└┘ └─────────┘└───────────
doc     └──────────┘└────────────┘└┘            └───────────
txt     └──────────┘              └┘            └───────────
par     └──────────┘              └┘            └───────────
pid          └──┘└┘              └┘            └─────────┘
st     └────────────────────────────────────────────────────
360    using frontier_inter_subset (-s) (-t)
id           └───────────────────┘      
src  ───────┘└───────────────────┘  └┘   └─
typ  ───────┘└───────────────────┘ └┘  └─
doc  ───────┘                        └┘   └─
txt  ───────┘                        └┘   └─
par  ───────┘                        └┘   └─
pid  ─┘└────┘                        └┘   
st   ────────────────────────────────────────
361  
src  
typ  
doc  
txt  
par  
pid  
st   
362  lemma is_closed.frontier_eq {s : set α} (hs : is_closed s) : frontier s = s \ interior s :=
id                                    └─┘         └───────┘     └──────┘     └──────┘ 
src                                   └─┘          └───────┘      └──────┘       └──────┘
typ                                   └─┘         └───────┘     └──────┘     └──────┘ 
doc                                                └───────┘      └──────┘         └──────┘
363  by rw [frontier, closure_eq_of_is_closed hs]
id          └──────┘  └─────────────────────┘ └┘
src     └──┘└──────┘└┘└─────────────────────┘  └─
typ     └──┘└──────┘└┘└─────────────────────┘└┘└─
doc     └──┘└──────┘└┘                         └─
txt     └──┘        └┘                         └─
par     └──┘        └┘                         └─
pid       └┘        └┘                         
st     └───────────┘└──────────────────────────┘
364  
src  
typ  
doc  
txt  
par  
pid  
st   
365  lemma is_open.frontier_eq {s : set α} (hs : is_open s) : frontier s = closure s \ s :=
id                                  └─┘         └─────┘     └──────┘   └─────┘   
src                                 └─┘          └─────┘      └──────┘    └─────┘   
typ                                 └─┘         └─────┘     └──────┘   └─────┘   
doc                                              └─────┘      └──────┘     └─────┘
366  by rw [frontier, interior_eq_of_open hs]
id          └──────┘  └─────────────────┘ └┘
src     └──┘└──────┘└┘└─────────────────┘  └─
typ     └──┘└──────┘└┘└─────────────────┘└┘└─
doc     └──┘└──────┘└┘                     └─
txt     └──┘        └┘                     └─
par     └──┘        └┘                     └─
pid       └┘        └┘                     
st     └───────────┘└──────────────────────┘
367  
src  
typ  
doc  
txt  
par  
pid  
st   
368  /-- The frontier of a set is closed. -/
369  lemma is_closed_frontier {s : set α} : is_closed (frontier s) :=
id                                 └─┘     └───────┘  └──────┘ 
src                                └─┘      └───────┘  └──────┘
typ                                └─┘     └───────┘  └──────┘ 
doc                                         └───────┘  └──────┘
370  by rw frontier_eq_closure_inter_closure; exact is_closed_inter is_closed_closure is_closed_closure
id         └───────────────────────────────┘        └─────────────┘                   └───────────────┘
src     └─┘└───────────────────────────────┘  └────┘└─────────────┘                 └───────────────┘
typ     └─┘└───────────────────────────────┘  └────┘└─────────────┘                 └───────────────┘
doc     └─┘                                   └────┘                                                 
txt     └─┘                                   └────┘                                                 
par     └─┘                                   └────┘                                                 
pid                                                                                                
st     └────────────────────────────────────────────────────────────────────────────────────────────────
371  
src  
typ  
doc  
txt  
par  
pid  
st   
372  /-- The frontier of a set has no interior point. -/
373  lemma interior_frontier {s : set α} (h : is_closed s) : interior (frontier s) = ∅ :=
id                                └─┘        └───────┘     └──────┘  └──────┘    
src                               └─┘         └───────┘      └──────┘  └──────┘     
typ                               └─┘        └───────┘     └──────┘  └──────┘    
doc                                           └───────┘      └──────┘  └──────┘
374  begin
st   └─────
375    have A : frontier s = s \ interior s, from h.frontier_eq,
id              └──────┘       └──────┘        └───────────┘
src    └───────┘└──────┘  └──────┘   └───┘└───────────┘
typ    └───────┘└──────┘  └──────┘  └───┘└───────────┘
doc    └───────┘└──────┘    └──────┘   └───┘
txt    └───────┘                       └───┘
par    └───────┘                       └───┘
pid    └────┘└─┘                       └───┘
st   ─────────────────────────────────────┘└──────────────────┘└─
376    have B : interior (frontier s) ⊆ interior s, by rw A; exact interior_mono (diff_subset _ _),
id                        └──────┘     └──────┘                 └───────────┘  └─────────┘
src    └───────┘         └──────┘ └┘└──────┘      └─┘   └────┘└───────────┘ └─────────┘└───┘
typ    └───────┘         └──────┘ └┘└──────┘     └─┘  └────┘└───────────┘ └─────────┘└───┘
doc    └───────┘         └──────┘ └┘ └──────┘      └─┘   └────┘                         └───┘
txt    └───────┘                  └┘               └─┘   └────┘                         └───┘
par    └───────┘                  └┘               └─┘   └────┘                         └───┘
pid    └────┘└─┘                  └┘                                                  └───┘
st   ────────────────────────────────────────────┘                                               └─
377    have C : interior (frontier s) ⊆ frontier s := interior_subset,
id              └──────┘                └──────┘     └─────────────┘
src    └───────┘└──────┘          └┘ └──────┘ └──┘└─────────────┘
typ    └───────┘└──────┘          └┘ └──────┘└──┘└─────────────┘
doc    └───────┘└──────┘          └┘ └──────┘ └──┘
txt    └───────┘                  └┘          └──┘
par    └───────┘                  └┘          └──┘
pid    └────┘└─┘                  └┘          └──┘
st   ───────────────────────────────────────────────────────────────┘└─
378    have : interior (frontier s) ⊆ (interior s) ∩ (s \ interior s) :=
id                      └──────┘                         └──────┘ 
src    └─────┘         └──────┘ └┘           └┘   └──────┘ └────
typ    └─────┘         └──────┘ └┘           └┘   └──────┘└────
doc    └─────┘         └──────┘ └┘           └┘    └──────┘ └────
txt    └─────┘                  └┘           └┘             └────
par    └─────┘                  └┘           └┘             └────
pid    └───┘└┘                  └┘           └┘             └───
st   ────────────────────────────────────────────────────────────────────
379      subset_inter B (by simpa [A] using C),
id       └──────────┘                     
src  ───┘└──────────┘    └─────┘ └──────┘ 
typ  ───┘└──────────┘   └─────┘└──────┘
doc  ───┘                └─────┘ └──────┘ 
txt  ───┘                └─────┘ └──────┘ 
par  ───┘                └─────┘ └──────┘ 
pid  ───┘                └──────┘ └──────┘ 
st   ─────────────────────┘└────────────────┘└─
380    rwa [inter_diff_self, subset_empty_iff] at this,
id          └─────────────┘  └──────────────┘
src    └───┘└─────────────┘└┘└──────────────┘└───────┘
typ    └───┘└─────────────┘└┘└──────────────┘└───────┘
doc    └───┘               └┘                └───────┘
txt    └───┘               └┘                └───────┘
par    └───┘               └┘                └───────┘
pid       └┘               └┘                └──────┘
st   ─────────────────────┘└────────────────┘└──────┘└─
381  end
st   ──┘
382  
383  /-- neighbourhood filter -/
384  def nhds (a : α) : filter α := (⨅ s ∈ {s : set α | a ∈ s ∧ is_open s}, principal s)
id                     └────┘              └─┘        └─────┘   └───────┘ 
src                     └────┘                └─┘           └─────┘    └───────┘
typ                    └────┘              └─┘        └─────┘   └───────┘ 
doc                                                            └─────┘    └───────┘
385  
386  localized "notation `𝓝` := nhds" in topological_space
387  
388  lemma nhds_def (a : α) : 𝓝 a = (⨅ s ∈ {s : set α | a ∈ s ∧ is_open s}, principal s) := rfl
id                                       └─┘        └─────┘   └───────┘      └─┘
src                                         └─┘           └─────┘    └───────┘       └─┘
typ                                      └─┘        └─────┘   └───────┘      └─┘
doc                                                           └─────┘    └───────┘
389  
390  lemma le_nhds_iff {f a} : f ≤ 𝓝 a ↔ ∀ s : set α, a ∈ s → is_open s → s ∈ f :=
id                                        └─┘        └─────┘      
src                                         └─┘           └─────┘       
typ                                       └─┘        └─────┘      
doc                                                          └─────┘
391  by simp [nhds_def]
id            └──────┘
src     └────┘└──────┘└─
typ     └────┘└──────┘└─
doc     └────┘        └─
txt     └────┘        └─
par     └────┘        └─
pid                 
st     └────────────────
392  
src  
typ  
doc  
txt  
par  
pid  
st   
393  lemma nhds_le_of_le {f a} {s : set α} (h : a ∈ s) (o : is_open s) (sf : principal s ≤ f) : 𝓝 a ≤ f :=
id                                  └─┘                 └─────┘         └───────┘          
src                                 └─┘                    └─────┘          └───────┘            
typ                                 └─┘                 └─────┘         └───────┘          
doc                                                         └─────┘          └───────┘          
394  by rw nhds_def; exact infi_le_of_le s (infi_le_of_le ⟨h, o⟩ sf)
id         └──────┘                        └───────────┘      └┘
src     └─┘└──────┘  └────┘               └───────────┘  └┘ └┘  └─
typ     └─┘└──────┘  └────┘              └───────────┘ └┘└┘└┘└─
doc     └─┘          └────┘                              └┘ └┘  └─
txt     └─┘          └────┘                              └┘ └┘  └─
par     └─┘          └────┘                              └┘ └┘  └─
pid                                                    └┘ └┘  
st     └─────────────────────────────────────────────────────────────
395  
src  
typ  
doc  
txt  
par  
pid  
st   
396  lemma nhds_sets {a : α} : (𝓝 a).sets = {s | ∃t⊆s, is_open t ∧ a ∈ t} :=
id                               └──┘        └─────┘     
src                                └──┘           └─────┘      
typ                              └──┘        └─────┘     
doc                                                   └─────┘
397  calc (𝓝 a).sets = (⋃s∈{s : set α| a ∈ s ∧ is_open s}, (principal s).sets) : binfi_sets_eq
id           └──┘          └─┘       └─────┘    └───────┘  └──┘     └───────────┘
src           └──┘           └─┘          └─────┘     └───────┘   └──┘     └───────────┘
typ          └──┘          └─┘       └─────┘    └───────┘  └──┘     └───────────┘
doc                                          └─────┘     └───────┘
398    (assume x ⟨hx₁, hx₂⟩ y ⟨hy₁, hy₂⟩,
id              └─┘  └─┘   └─┘  └─┘
typ             └─┘  └─┘   └─┘  └─┘
399      ⟨x ∩ y, ⟨⟨hx₁, hy₁⟩, is_open_inter hx₂ hy₂⟩,
id                         └───────────┘
src                          └───────────┘
typ                        └───────────┘
400        le_principal_iff.2 (inter_subset_left _ _),
id         └──────────────┘   └───────────────┘
src        └──────────────┘   └───────────────┘
typ        └──────────────┘   └───────────────┘
401        le_principal_iff.2 (inter_subset_right _ _)⟩)
id         └──────────────┘   └────────────────┘
src        └──────────────┘   └────────────────┘
typ        └──────────────┘   └────────────────┘
402    ⟨univ, mem_univ _, is_open_univ⟩
id      └──┘  └──────┘    └──────────┘
src     └──┘  └──────┘    └──────────┘
typ     └──┘  └──────┘    └──────────┘
403    ... = {s | ∃t⊆s, is_open t ∧ a ∈ t} :
id                └─────┘     
src                  └─────┘      
typ               └─────┘     
doc                     └─────┘
404      le_antisymm
id       └─────────┘
src      └─────────┘
typ      └─────────┘
405        (supr_le $ assume i, supr_le $ assume ⟨hi₁, hi₂⟩ t ht, ⟨i, ht, hi₂, hi₁⟩)
id          └─────┘            └─────┘          └─┘  └─┘   └┘     └┘
src         └─────┘             └─────┘
typ         └─────┘            └─────┘          └─┘  └─┘   └┘     └┘
406        (assume t ⟨i, hi₁, hi₂, hi₃⟩, mem_Union.2 ⟨i, mem_Union.2 ⟨⟨hi₃, hi₂⟩, hi₁⟩⟩)
id                    └─┘  └─┘  └─┘   └───────┘      └───────┘
src                                      └───────┘      └───────┘
typ                   └─┘  └─┘  └─┘   └───────┘      └───────┘
407  
408  lemma map_nhds {a : α} {f : α → β} :
id                                 
typ                                
409    map f (𝓝 a) = (⨅ s ∈ {s : set α | a ∈ s ∧ is_open s}, principal (image f s)) :=
id     └─┘                └─┘        └─────┘   └───────┘  └───┘  
src    └─┘                   └─┘           └─────┘    └───────┘  └───┘
typ    └─┘                └─┘        └─────┘   └───────┘  └───┘  
doc    └─┘                                     └─────┘    └───────┘
410  calc map f (𝓝 a) = (⨅ s ∈ {s : set α | a ∈ s ∧ is_open s}, map f (principal s)) :
id        └─┘                 └─┘        └─────┘   └─┘   └───────┘ 
src       └─┘                    └─┘           └─────┘    └─┘    └───────┘
typ       └─┘                 └─┘        └─────┘   └─┘   └───────┘ 
doc       └─┘                                     └─────┘    └─┘    └───────┘
411      map_binfi_eq
id       └──────────┘
src      └──────────┘
typ      └──────────┘
412      (assume x ⟨hx₁, hx₂⟩ y ⟨hy₁, hy₂⟩,
id                └─┘  └─┘   └─┘  └─┘
typ               └─┘  └─┘   └─┘  └─┘
413        ⟨x ∩ y, ⟨⟨hx₁, hy₁⟩, is_open_inter hx₂ hy₂⟩,
id                           └───────────┘
src                            └───────────┘
typ                          └───────────┘
414        le_principal_iff.2 (inter_subset_left _ _),
id         └──────────────┘   └───────────────┘
src        └──────────────┘   └───────────────┘
typ        └──────────────┘   └───────────────┘
415        le_principal_iff.2 (inter_subset_right _ _)⟩)
id         └──────────────┘   └────────────────┘
src        └──────────────┘   └────────────────┘
typ        └──────────────┘   └────────────────┘
416      ⟨univ, mem_univ _, is_open_univ⟩
id        └──┘  └──────┘    └──────────┘
src       └──┘  └──────┘    └──────────┘
typ       └──┘  └──────┘    └──────────┘
417    ... = _ : by simp only [map_principal]
id                             └───────────┘
src                 └─────────┘└───────────┘└─
typ                 └─────────┘└───────────┘└─
doc                 └─────────┘             └─
txt                 └─────────┘             └─
par                 └─────────┘             └─
pid                     └──┘└┘             
st                 └──────────────────────────
418  
src  
typ  
doc  
txt  
par  
pid  
st   
419  attribute [irreducible] nhds
id                           └──┘
src                          └──┘
typ                          └──┘
doc             └─────────┘  └──┘
420  
421  lemma mem_nhds_sets_iff {a : α} {s : set α} :
id                                       └─┘ 
src                                       └─┘
typ                                      └─┘ 
422   s ∈ 𝓝 a ↔ ∃t⊆s, is_open t ∧ a ∈ t :=
id           └─────┘     
src              └─────┘      
typ          └─────┘     
doc                  └─────┘
423  by simp only [nhds_sets, mem_set_of_eq, exists_prop]
id                 └───────┘  └───────────┘  └─────────┘
src     └─────────┘└───────┘└┘└───────────┘└┘└─────────┘└─
typ     └─────────┘└───────┘└┘└───────────┘└┘└─────────┘└─
doc     └─────────┘         └┘             └┘           └─
txt     └─────────┘         └┘             └┘           └─
par     └─────────┘         └┘             └┘           └─
pid         └──┘└┘         └┘             └┘           
st     └──────────────────────────────────────────────────
424  
src  
typ  
doc  
txt  
par  
pid  
st   
425  lemma mem_of_nhds {a : α} {s : set α} : s ∈ 𝓝 a → a ∈ s :=
id                                 └─┘             
src                                 └─┘                
typ                                └─┘             
doc                                              
426  λ H, let ⟨t, ht, _, hs⟩ := mem_nhds_sets_iff.1 H in ht hs
id       └─┘     └┘     └┘     └───────────────┘  
src                             └───────────────┘
typ      └─┘     └┘     └┘     └───────────────┘  
427  
428  lemma mem_nhds_sets {a : α} {s : set α} (hs : is_open s) (ha : a ∈ s) :
id                                   └─┘         └─────┘           
src                                   └─┘          └─────┘            
typ                                  └─┘         └─────┘           
doc                                                └─────┘
429   s ∈ 𝓝 a :=
id       
src      
typ      
doc       
430  mem_nhds_sets_iff.2 ⟨s, subset.refl _, hs, ha⟩
id   └───────────────┘     └─────────┘    └┘  └┘
src  └───────────────┘      └─────────┘
typ  └───────────────┘     └─────────┘    └┘  └┘
431  
432  theorem all_mem_nhds (x : α) (P : set α → Prop) (hP : ∀ s t, s ⊆ t → P s → P t) :
id                                    └─┘                               
src                                    └─┘                          
typ                                   └─┘                               
433    (∀ s ∈ 𝓝 x, P s) ↔ (∀ s, is_open s → x ∈ s → P s) :=
id                       └─────┘          
src                           └─────┘       
typ                      └─────┘          
doc                            └─────┘
434  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
435    (λ h s os xs, h s (mem_nhds_sets os xs))
id          └┘ └┘     └───────────┘ └┘ └┘
src                       └───────────┘
typ         └┘ └┘     └───────────┘ └┘ └┘
436    (λ h t,
id         
typ        
437      begin
st       └─────
438        change t ∈ (𝓝 x).sets → P t,
id                               
src        └─────┘   └─────┘  
typ        └─────┘  └─────┘ 
doc        └─────┘    └─────┘  
txt        └─────┘     └─────┘  
par        └─────┘     └─────┘  
pid                   └─────┘  
st   ────────────────────────────────┘└─
439        rw nhds_sets,
id            └───────┘
src        └─┘└───────┘
typ        └─┘└───────┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ─────────────────┘└─
440        rintros ⟨s, hs, opens, xs⟩,
src        └────────────────────────┘
typ        └────────────────────────┘
doc        └────────────────────────┘
txt        └────────────────────────┘
par        └────────────────────────┘
pid               └─────────────────┘
st   ───────────────────────────────┘└─
441        exact hP _ _ hs (h s opens xs),
id               └┘     └┘    └───┘ └┘
src        └────┘  └───┘            
typ        └────┘└┘└───┘└┘ └───┘└┘
doc        └────┘  └───┘            
txt        └────┘  └───┘            
par        └────┘  └───┘            
pid               └───┘            
st   ───────────────────────────────────┘└─
442      end)
st   ──────┘
443  
444  theorem all_mem_nhds_filter (x : α) (f : set α → set β) (hf : ∀ s t, s ⊆ t → f s ⊆ f t)
id                                           └─┘    └─┘                       
src                                           └─┘     └─┘                            
typ                                          └─┘    └─┘                       
445      (l : filter β) :
id            └────┘ 
src           └────┘
typ           └────┘ 
446    (∀ s ∈ 𝓝 x, f s ∈ l) ↔ (∀ s, is_open s → x ∈ s → f s ∈ l) :=
id                         └─────┘            
src                              └─────┘                
typ                        └─────┘            
doc                                └─────┘
447  all_mem_nhds _ _ (λ s t ssubt h, mem_sets_of_superset h (hf s t ssubt))
id   └──────────┘          └───┘   └──────────────────┘   └┘   └───┘
src  └──────────┘                     └──────────────────┘
typ  └──────────┘          └───┘   └──────────────────┘   └┘   └───┘
448  
449  theorem rtendsto_nhds {r : rel β α} {l : filter β} {a : α} :
id                              └─┘         └────┘        
src                             └─┘           └────┘
typ                             └─┘         └────┘        
doc                             └─┘
450    rtendsto r l (𝓝 a) ↔ (∀ s, is_open s → a ∈ s → r.core s ∈ l) :=
id     └──────┘             └─────┘         └───┘   
src    └──────┘                 └─────┘             └───┘   
typ    └──────┘             └─────┘         └───┘   
doc                              └─────┘              └───┘
451  all_mem_nhds_filter _ _ (λ s t, id) _
id   └─────────────────┘           └┘
src  └─────────────────┘             └┘
typ  └─────────────────┘           └┘
452  
453  theorem rtendsto'_nhds {r : rel β α} {l : filter β} {a : α} :
id                               └─┘         └────┘        
src                              └─┘           └────┘
typ                              └─┘         └────┘        
doc                              └─┘
454    rtendsto' r l (𝓝 a) ↔ (∀ s, is_open s → a ∈ s → r.preimage s ∈ l) :=
id     └───────┘             └─────┘         └───────┘   
src    └───────┘                 └─────┘             └───────┘   
typ    └───────┘             └─────┘         └───────┘   
doc                               └─────┘              └───────┘
455  by { rw [rtendsto'_def], apply all_mem_nhds_filter, apply rel.preimage_mono }
id            └───────────┘         └─────────────────┘        └───────────────┘
src       └──┘└───────────┘  └────┘└─────────────────┘  └────┘└───────────────┘
typ       └──┘└───────────┘  └────┘└─────────────────┘  └────┘└───────────────┘
doc       └──┘               └────┘                     └────┘                 
txt       └──┘               └────┘                     └────┘                 
par       └──┘               └────┘                     └────┘                 
pid         └┘                                                               
st     └──────────────────┘└──────────────────────────┘└────────────────────────┘└┘
456  
457  theorem ptendsto_nhds {f : β →. α} {l : filter β} {a : α} :
id                               └┘        └────┘        
src                               └┘         └────┘
typ                              └┘        └────┘        
doc                               └┘
458    ptendsto f l (𝓝 a) ↔ (∀ s, is_open s → a ∈ s → f.core s ∈ l) :=
id     └──────┘             └─────┘         └───┘   
src    └──────┘                 └─────┘             └───┘   
typ    └──────┘             └─────┘         └───┘   
doc                              └─────┘
459  rtendsto_nhds
id   └───────────┘
src  └───────────┘
typ  └───────────┘
460  
461  theorem ptendsto'_nhds {f : β →. α} {l : filter β} {a : α} :
id                                └┘        └────┘        
src                                └┘         └────┘
typ                               └┘        └────┘        
doc                                └┘
462    ptendsto' f l (𝓝 a) ↔ (∀ s, is_open s → a ∈ s → f.preimage s ∈ l) :=
id     └───────┘             └─────┘         └───────┘   
src    └───────┘                 └─────┘             └───────┘   
typ    └───────┘             └─────┘         └───────┘   
doc                               └─────┘
463  rtendsto'_nhds
id   └────────────┘
src  └────────────┘
typ  └────────────┘
464  
465  theorem tendsto_nhds {f : β → α} {l : filter β} {a : α} :
id                                       └────┘        
src                                        └────┘
typ                                      └────┘        
466    tendsto f l (𝓝 a) ↔ (∀ s, is_open s → a ∈ s → f ⁻¹' s ∈ l) :=
id     └─────┘             └─────┘          └─┘   
src    └─────┘                 └─────┘              └─┘   
typ    └─────┘             └─────┘          └─┘   
doc    └─────┘                  └─────┘               └─┘
467  all_mem_nhds_filter _ _ (λ s t h, preimage_mono h) _
id   └─────────────────┘            └───────────┘ 
src  └─────────────────┘               └───────────┘
typ  └─────────────────┘            └───────────┘ 
468  
469  lemma tendsto_const_nhds {a : α} {f : filter β} : tendsto (λb:β, a) f (𝓝 a) :=
id                                        └────┘     └─────┘            
src                                        └────┘      └─────┘              
typ                                       └────┘     └─────┘            
doc                                                    └─────┘              
470  tendsto_nhds.mpr $ assume s hs ha, univ_mem_sets' $ assume _, ha
id   └──────────┘└──┘           └┘ └┘  └────────────┘            └┘
src  └──────────┘└──┘                   └────────────┘
typ  └──────────┘└──┘           └┘ └┘  └────────────┘            └┘
471  
472  lemma pure_le_nhds : pure ≤ (𝓝 : α → filter α) :=
id                        └──┘         └────┘ 
src                       └──┘          └────┘
typ                       └──┘         └────┘ 
doc                               
473  assume a s hs, mem_pure_sets.2 $ mem_of_nhds hs
id            └┘  └───────────┘    └─────────┘ └┘
src                 └───────────┘    └─────────┘
typ           └┘  └───────────┘    └─────────┘ └┘
474  
475  lemma tendsto_pure_nhds {α : Type*} [topological_space β] (f : α → β) (a : α) :
id                                        └───────────────┘                  
src                                       └───────────────┘
typ                                       └───────────────┘                  
doc                                       └───────────────┘
476    tendsto f (pure a) (𝓝 (f a)) :=
id     └─────┘   └──┘       
src    └─────┘    └──┘     
typ    └─────┘   └──┘       
doc    └─────┘             
477  begin
st   └─────
478    rw [tendsto, filter.map_pure],
id         └─────┘  └─────────────┘
src    └──┘└─────┘└┘└─────────────┘
typ    └──┘└─────┘└┘└─────────────┘
doc    └──┘└─────┘└┘               
txt    └──┘       └┘               
par    └──┘       └┘               
pid      └┘       └┘               
st   ────────────┘└───────────────┘└──
479    exact pure_le_nhds (f a)
id           └──────────┘   
src    └────┘└──────────┘   └┘
typ    └────┘└──────────┘ └┘
doc    └────┘               └┘
txt    └────┘               └┘
par    └────┘               └┘
pid                        
st   ──────────────────────────┘
480  end
st   └─┘
481  
482  @[simp] lemma nhds_ne_bot {a : α} : 𝓝 a ≠ ⊥ :=
id                                         
src                                          
typ                                        
doc    └──┘                              
483  ne_bot_of_le_ne_bot pure_ne_bot (pure_le_nhds a)
id   └─────────────────┘ └─────────┘  └──────────┘ 
src  └─────────────────┘ └─────────┘  └──────────┘
typ  └─────────────────┘ └─────────┘  └──────────┘ 
484  
485  lemma interior_eq_nhds {s : set α} : interior s = {a | 𝓝 a ≤ principal s} :=
id                               └─┘     └──────┘         └───────┘ 
src                              └─┘      └──────┘            └───────┘
typ                              └─┘     └──────┘         └───────┘ 
doc                                       └──────┘               └───────┘
486  set.ext $ λ x, by simp only [mem_interior, le_principal_iff, mem_nhds_sets_iff]; refl
id   └─────┘                     └──────────┘  └──────────────┘  └───────────────┘
src  └─────┘           └─────────┘└──────────┘└┘└──────────────┘└┘└───────────────┘  └────
typ  └─────┘          └─────────┘└──────────┘└┘└──────────────┘└┘└───────────────┘  └────
doc                    └─────────┘            └┘                └┘                   └────
txt                    └─────────┘            └┘                └┘                   └────
par                    └─────────┘            └┘                └┘                   └────
pid                        └──┘└┘            └┘                └┘                       
st                    └────────────────────────────────────────────────────────────────────
487  
src  
typ  
doc  
txt  
par  
pid  
st   
488  lemma mem_interior_iff_mem_nhds {s : set α} {a : α} :
id                                        └─┘        
src                                       └─┘
typ                                       └─┘        
489    a ∈ interior s ↔ s ∈ 𝓝 a :=
id       └──────┘      
src       └──────┘       
typ      └──────┘      
doc        └──────┘         
490  by simp only [interior_eq_nhds, le_principal_iff]; refl
id                 └──────────────┘  └──────────────┘
src     └─────────┘└──────────────┘└┘└──────────────┘  └────
typ     └─────────┘└──────────────┘└┘└──────────────┘  └────
doc     └─────────┘                └┘                  └────
txt     └─────────┘                └┘                  └────
par     └─────────┘                └┘                  └────
pid         └──┘└┘                └┘                      
st     └─────────────────────────────────────────────────────
491  
src  
typ  
doc  
txt  
par  
pid  
st   
492  lemma is_open_iff_nhds {s : set α} : is_open s ↔ ∀a∈s, 𝓝 a ≤ principal s :=
id                               └─┘     └─────┘          └───────┘ 
src                              └─┘      └─────┘              └───────┘
typ                              └─┘     └─────┘          └───────┘ 
doc                                       └─────┘                └───────┘
493  calc is_open s ↔ s ⊆ interior s : subset_interior_iff_open.symm
id        └─────┘      └──────┘    └──────────────────────┘└───┘
src       └─────┘        └──────┘     └──────────────────────┘└───┘
typ       └─────┘      └──────┘    └──────────────────────┘└───┘
doc       └─────┘         └──────┘
494    ... ↔ (∀a∈s, 𝓝 a ≤ principal s) : by rw [interior_eq_nhds]; refl
id                   └───────┘            └──────────────┘
src                     └───────┘         └──┘└──────────────┘  └────
typ                  └───────┘        └──┘└──────────────┘  └────
doc                      └───────┘         └──┘                  └────
txt                                         └──┘                  └────
par                                         └──┘                  └────
pid                                           └┘                      
st                                         └───────────────────┘└──────
495  
src  
typ  
doc  
txt  
par  
pid  
st   
496  lemma is_open_iff_mem_nhds {s : set α} : is_open s ↔ ∀a∈s, s ∈ 𝓝 a :=
id                                   └─┘     └─────┘          
src                                  └─┘      └─────┘             
typ                                  └─┘     └─────┘          
doc                                           └─────┘               
497  is_open_iff_nhds.trans $ forall_congr $ λ _, imp_congr_right $ λ _, le_principal_iff
id   └──────────────┘└────┘   └──────────┘       └─────────────┘       └──────────────┘
src  └──────────────┘└────┘   └──────────┘        └─────────────┘        └──────────────┘
typ  └──────────────┘└────┘   └──────────┘       └─────────────┘       └──────────────┘
498  
499  lemma closure_eq_nhds {s : set α} : closure s = {a | 𝓝 a ⊓ principal s ≠ ⊥} :=
id                              └─┘     └─────┘         └───────┘   
src                             └─┘      └─────┘            └───────┘    
typ                             └─┘     └─────┘         └───────┘   
doc                                      └─────┘               └───────┘
500  calc closure s = - interior (- s) : closure_eq_compl_interior_compl
id        └─────┘     └──────┘       └─────────────────────────────┘
src       └─────┘      └──────┘        └─────────────────────────────┘
typ       └─────┘     └──────┘       └─────────────────────────────┘
doc       └─────┘       └──────┘
501    ... = {a | ¬ 𝓝 a ≤ principal (-s)} : by rw [interior_eq_nhds]; refl
id                  └───────┘              └──────────────┘
src                   └───────┘           └──┘└──────────────┘  └────
typ                 └───────┘          └──┘└──────────────┘  └────
doc                      └───────┘            └──┘                  └────
txt                                            └──┘                  └────
par                                            └──┘                  └────
pid                                              └┘                      
st                                            └───────────────────┘└──────
502    ... = {a | 𝓝 a ⊓ principal s ≠ ⊥} : set.ext $ assume a, not_congr
id                 └───────┘       └─────┘            └───────┘
src  ─┘              └───────┘        └─────┘             └───────┘
typ  ─┘            └───────┘       └─────┘            └───────┘
doc  ─┘                └───────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
503      (inf_eq_bot_iff_le_compl
id        └─────────────────────┘
src       └─────────────────────┘
typ       └─────────────────────┘
504        (show principal s ⊔ principal (-s) = ⊤, by simp only [sup_principal, union_compl_self, principal_univ])
id               └───────┘   └───────┘                     └───────────┘  └──────────────┘  └────────────┘
src              └───────┘    └───────┘           └─────────┘└───────────┘└┘└──────────────┘└┘└────────────┘
typ              └───────┘   └───────┘          └─────────┘└───────────┘└┘└──────────────┘└┘└────────────┘
doc              └───────┘     └───────┘              └─────────┘             └┘                └┘              
txt                                                   └─────────┘             └┘                └┘              
par                                                   └─────────┘             └┘                └┘              
pid                                                       └──┘└┘             └┘                └┘              
st                                                   └──────────────────────────────────────────────────────────┘
505        (by simp only [inf_principal, inter_compl_self, principal_empty])).symm
id                        └───────────┘  └──────────────┘  └─────────────┘   └──┘
src            └─────────┘└───────────┘└┘└──────────────┘└┘└─────────────┘  └──┘
typ            └─────────┘└───────────┘└┘└──────────────┘└┘└─────────────┘  └──┘
doc            └─────────┘             └┘                └┘               
txt            └─────────┘             └┘                └┘               
par            └─────────┘             └┘                └┘               
pid                └──┘└┘             └┘                └┘               
st            └───────────────────────────────────────────────────────────┘
506  
507  theorem mem_closure_iff_nhds {s : set α} {a : α} :
id                                     └─┘        
src                                    └─┘
typ                                    └─┘        
508    a ∈ closure s ↔ ∀ t ∈ 𝓝 a, (t ∩ s).nonempty :=
id       └─────┘               └──────┘
src       └─────┘                    └──────┘
typ      └─────┘               └──────┘
doc        └─────┘                      └──────┘
509  mem_closure_iff.trans
id   └─────────────┘└────┘
src  └─────────────┘└────┘
typ  └─────────────┘└────┘
510  ⟨λ H t ht, nonempty.mono
id        └┘  └───────────┘
src             └───────────┘
typ       └┘  └───────────┘
511    (inter_subset_inter_left _ interior_subset)
id      └─────────────────────┘   └─────────────┘
src     └─────────────────────┘   └─────────────┘
typ     └─────────────────────┘   └─────────────┘
512    (H _ is_open_interior (mem_interior_iff_mem_nhds.2 ht)),
id         └──────────────┘  └───────────────────────┘  └┘
src         └──────────────┘  └───────────────────────┘
typ        └──────────────┘  └───────────────────────┘  └┘
513   λ H o oo ao, H _ (mem_nhds_sets oo ao)⟩
id        └┘ └┘      └───────────┘ └┘ └┘
src                     └───────────┘
typ       └┘ └┘      └───────────┘ └┘ └┘
514  
515  /-- `x` belongs to the closure of `s` if and only if some ultrafilter
516    supported on `s` converges to `x`. -/
517  lemma mem_closure_iff_ultrafilter {s : set α} {x : α} :
id                                          └─┘        
src                                         └─┘
typ                                         └─┘        
518    x ∈ closure s ↔ ∃ (u : ultrafilter α), s ∈ u.val ∧ u.val ≤ 𝓝 x :=
id       └─────┘         └─────────┘     └──┘  └──┘   
src       └─────┘          └─────────┘        └──┘   └──┘  
typ      └─────┘         └─────────┘     └──┘  └──┘   
doc        └─────┘            └─────────┘                         
519  begin
st   └─────
520    rw closure_eq_nhds, change 𝓝 x ⊓ principal s ≠ ⊥ ↔ _, symmetry,
id        └─────────────┘            └───────┘   
src    └─┘└─────────────┘  └─────┘ └───────┘  └┘  └──────┘
typ    └─┘└─────────────┘  └─────┘└───────┘ └┘  └──────┘
doc    └─┘                 └─────┘  └───────┘    └┘  └──────┘
txt    └─┘                 └─────┘                └┘  └──────┘
par    └─┘                 └─────┘                └┘  └──────┘
pid                                             └┘
st   ───────────────────┘└────────────────────────────────┘└────────┘└─
521    convert exists_ultrafilter_iff _, ext u,
id             └────────────────────┘
src    └──────┘└────────────────────┘└┘  └───┘
typ    └──────┘└────────────────────┘└┘  └───┘
doc    └──────┘                      └┘  └───┘
txt    └──────┘                      └┘  └───┘
par    └──────┘                      └┘  └───┘
pid                                 └┘     └┘
st   ─────────────────────────────────┘└─────┘└─
522    rw [←le_principal_iff, inf_comm, le_inf_iff]
id          └──────────────┘  └──────┘  └────────┘
src    └───┘└──────────────┘└┘└──────┘└┘└────────┘└┘
typ    └───┘└──────────────┘└┘└──────┘└┘└────────┘└┘
doc    └───┘                └┘        └┘          └┘
txt    └───┘                └┘        └┘          └┘
par    └───┘                └┘        └┘          └┘
pid      └─┘                └┘        └┘          
st   ──────────────────────┘└────────┘└──────────┘
523  end
st   └─┘
524  
525  lemma is_closed_iff_nhds {s : set α} : is_closed s ↔ ∀a, 𝓝 a ⊓ principal s ≠ ⊥ → a ∈ s :=
id                                 └─┘     └───────┘         └───────┘        
src                                └─┘      └───────┘            └───────┘         
typ                                └─┘     └───────┘         └───────┘        
doc                                         └───────┘              └───────┘
526  calc is_closed s ↔ closure s = s : by rw [closure_eq_iff_is_closed]
id        └───────┘    └─────┘             └──────────────────────┘
src       └───────┘     └─────┘           └──┘└──────────────────────┘└─
typ       └───────┘    └─────┘         └──┘└──────────────────────┘└─
doc       └───────┘     └─────┘            └──┘                        └─
txt                                        └──┘                        └─
par                                        └──┘                        └─
pid                                          └┘                        
st                                        └───────────────────────────┘
527    ... ↔ closure s ⊆ s : ⟨assume h, by rw h, assume h, subset.antisymm h subset_closure⟩
id           └─────┘                                 └─────────────┘  └────────────┘
src  ─┘      └─────┘                      └─┘             └─────────────┘   └────────────┘
typ  ─┘      └─────┘                   └─┘           └─────────────┘  └────────────┘
doc  ─┘      └─────┘                       └─┘
txt  ─┘                                    └─┘
par  ─┘                                    └─┘
pid  ─┘                                      
st   ─┘                                   └───┘
528    ... ↔ (∀a, 𝓝 a ⊓ principal s ≠ ⊥ → a ∈ s) : by rw [closure_eq_nhds]; refl
id                  └───────┘                   └─────────────┘
src                   └───────┘                  └──┘└─────────────┘  └────
typ                 └───────┘               └──┘└─────────────┘  └────
doc                    └───────┘                     └──┘                 └────
txt                                                   └──┘                 └────
par                                                   └──┘                 └────
pid                                                     └┘                     
st                                                   └──────────────────┘└──────
529  
src  
typ  
doc  
txt  
par  
pid  
st   
530  lemma closure_inter_open {s t : set α} (h : is_open s) : s ∩ closure t ⊆ closure (s ∩ t) :=
id                                   └─┘        └─────┘       └─────┘   └─────┘    
src                                  └─┘         └─────┘         └─────┘    └─────┘    
typ                                  └─┘        └─────┘       └─────┘   └─────┘    
doc                                              └─────┘          └─────┘     └─────┘
531  assume a ⟨hs, ht⟩,
id           └┘
typ          └┘
532  have s ∈ 𝓝 a, from mem_nhds_sets h hs,
id                  └───────────┘ 
src                   └───────────┘
typ                 └───────────┘ 
doc           
533  have 𝓝 a ⊓ principal s = 𝓝 a, from inf_of_le_left $ by rwa le_principal_iff,
id           └───────┘           └────────────┘          └──────────────┘
src           └───────┘             └────────────┘      └──┘└──────────────┘
typ          └───────┘           └────────────┘      └──┘└──────────────┘
doc            └───────┘                                  └──┘
txt                                                         └──┘
par                                                         └──┘
pid                                                            
st                                                         └───────────────────┘
534  have 𝓝 a ⊓ principal (s ∩ t) ≠ ⊥,
id           └───────┘       
src           └───────┘         
typ          └───────┘       
doc            └───────┘
535    from calc 𝓝 a ⊓ principal (s ∩ t) = 𝓝 a ⊓ (principal s ⊓ principal t) : by rw inf_principal
id                  └───────┘            └───────┘   └───────┘           └───────────┘
src                  └───────┘               └───────┘    └───────┘         └─┘└───────────┘
typ                 └───────┘            └───────┘   └───────┘        └─┘└───────────┘
doc                   └───────┘                 └───────┘     └───────┘         └─┘             
txt                                                                               └─┘             
par                                                                               └─┘             
pid                                                                                              
st                                                                               └─────────────────
536      ... = 𝓝 a ⊓ principal t : by rw [←inf_assoc, this]
id                └───────┘            └───────┘  └──┘
src  ───┘          └───────┘        └───┘└───────┘└┘    └─
typ  ───┘         └───────┘       └───┘└───────┘└┘└──┘└─
doc  ───┘           └───────┘        └───┘         └┘    └─
txt  ───┘                             └───┘         └┘    └─
par  ───┘                             └───┘         └┘    └─
pid  ───┘                               └─┘         └┘    
st   ───┘                            └─────────────┘└────┘
537      ... ≠ ⊥ : by rw [closure_eq_nhds] at ht; assumption,
id                       └─────────────┘
src  ───┘            └──┘└─────────────┘└─────┘  └────────┘
typ  ───┘            └──┘└─────────────┘└─────┘  └────────┘
doc  ───┘             └──┘               └─────┘  └────────┘
txt  ───┘             └──┘               └─────┘  └────────┘
par  ───┘             └──┘               └─────┘  └────────┘
pid  ───┘               └┘               └────┘
st   ───┘            └──────────────────┘└────────────────┘
538  by rw [closure_eq_nhds]; assumption
id          └─────────────┘
src     └──┘└─────────────┘  └──────────
typ     └──┘└─────────────┘  └──────────
doc     └──┘                 └──────────
txt     └──┘                 └──────────
par     └──┘                 └──────────
pid       └┘                           
st     └──────────────────┘└────────────
539  
src  
typ  
doc  
txt  
par  
pid  
st   
540  lemma closure_diff {s t : set α} : closure s - closure t ⊆ closure (s - t) :=
id                             └─┘     └─────┘   └─────┘   └─────┘    
src                            └─┘      └─────┘    └─────┘    └─────┘    
typ                            └─┘     └─────┘   └─────┘   └─────┘    
doc                                     └─────┘     └─────┘     └─────┘
541  calc closure s \ closure t = (- closure t) ∩ closure s : by simp only [diff_eq, inter_comm]
id        └─────┘   └─────┘      └─────┘    └─────┘                  └─────┘  └────────┘
src       └─────┘    └─────┘       └─────┘     └─────┘        └─────────┘└─────┘└┘└────────┘└─
typ       └─────┘   └─────┘      └─────┘    └─────┘       └─────────┘└─────┘└┘└────────┘└─
doc       └─────┘     └─────┘        └─────┘      └─────┘        └─────────┘       └┘          └─
txt                                                              └─────────┘       └┘          └─
par                                                              └─────────┘       └┘          └─
pid                                                                  └──┘└┘       └┘          
st                                                              └────────────────────────────────
542    ... ⊆ closure (- closure t ∩ s) : closure_inter_open $ is_open_compl_iff.mpr $ is_closed_closure
id           └─────┘   └─────┘       └────────────────┘   └───────────────┘└──┘   └───────────────┘
src  ─┘      └─────┘   └─────┘         └────────────────┘   └───────────────┘└──┘   └───────────────┘
typ  ─┘      └─────┘   └─────┘       └────────────────┘   └───────────────┘└──┘   └───────────────┘
doc  ─┘      └─────┘    └─────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
543    ... = closure (s \ closure t) : by simp only [diff_eq, inter_comm]
id           └─────┘    └─────┘                   └─────┘  └────────┘
src          └─────┘     └─────┘         └─────────┘└─────┘└┘└────────┘└─
typ          └─────┘    └─────┘        └─────────┘└─────┘└┘└────────┘└─
doc          └─────┘      └─────┘         └─────────┘       └┘          └─
txt                                       └─────────┘       └┘          └─
par                                       └─────────┘       └┘          └─
pid                                           └──┘└┘       └┘          
st                                       └────────────────────────────────
544    ... ⊆ closure (s \ t) : closure_mono $ diff_subset_diff (subset.refl s) subset_closure
id           └─────┘        └──────────┘   └──────────────┘  └─────────┘   └────────────┘
src  ─┘      └─────┘          └──────────┘   └──────────────┘  └─────────┘    └────────────┘
typ  ─┘      └─────┘        └──────────┘   └──────────────┘  └─────────┘   └────────────┘
doc  ─┘      └─────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
545  
546  lemma mem_of_closed_of_tendsto {f : β → α} {b : filter β} {a : α} {s : set α}
id                                                 └────┘               └─┘ 
src                                                  └────┘                 └─┘
typ                                                └────┘               └─┘ 
547    (hb : b ≠ ⊥) (hf : tendsto f b (𝓝 a)) (hs : is_closed s) (h : f ⁻¹' s ∈ b) : a ∈ s :=
id                     └─────┘              └───────┘         └─┘         
src                     └─────┘                 └───────┘           └─┘           
typ                    └─────┘              └───────┘         └─┘         
doc                       └─────┘                 └───────┘           └─┘
548  have b.map f ≤ 𝓝 a ⊓ principal s,
id        └──┘      └───────┘ 
src        └──┘        └───────┘
typ       └──┘      └───────┘ 
doc        └──┘          └───────┘
549    from le_trans (le_inf (le_refl _) (le_principal_iff.mpr h)) (inf_le_inf hf (le_refl _)),
id          └──────┘  └────┘  └─────┘     └──────────────┘└──┘     └────────┘ └┘  └─────┘
src         └──────┘  └────┘  └─────┘     └──────────────┘└──┘      └────────┘     └─────┘
typ         └──────┘  └────┘  └─────┘     └──────────────┘└──┘     └────────┘ └┘  └─────┘
550  is_closed_iff_nhds.mp hs a $ ne_bot_of_le_ne_bot (map_ne_bot hb) this
id   └────────────────┘└─┘ └┘    └─────────────────┘  └────────┘ └┘  └──┘
src  └────────────────┘└─┘        └─────────────────┘  └────────┘
typ  └────────────────┘└─┘ └┘    └─────────────────┘  └────────┘ └┘  └──┘
551  
552  lemma mem_of_closed_of_tendsto' {f : β → α} {x : filter β} {a : α} {s : set α}
id                                                  └────┘               └─┘ 
src                                                   └────┘                 └─┘
typ                                                 └────┘               └─┘ 
553    (hf : tendsto f x (𝓝 a)) (hs : is_closed s) (h : x ⊓ principal (f ⁻¹' s) ≠ ⊥) : a ∈ s :=
id           └─────┘              └───────┘          └───────┘   └─┘          
src          └─────┘                 └───────┘            └───────┘    └─┘           
typ          └─────┘              └───────┘          └───────┘   └─┘          
doc          └─────┘                 └───────┘             └───────┘    └─┘
554  is_closed_iff_nhds.mp hs _ $ ne_bot_of_le_ne_bot (@map_ne_bot _ _ _ f h) $
id   └────────────────┘└─┘ └┘     └─────────────────┘   └────────┘        
src  └────────────────┘└─┘        └─────────────────┘   └────────┘
typ  └────────────────┘└─┘ └┘     └─────────────────┘   └────────┘        
555    le_inf (le_trans (map_mono $ inf_le_left) hf) $
id     └────┘  └──────┘  └──────┘   └─────────┘  └┘
src    └────┘  └──────┘  └──────┘   └─────────┘
typ    └────┘  └──────┘  └──────┘   └─────────┘  └┘
556      le_trans (map_mono $ inf_le_right_of_le $ by simp only [comap_principal, le_principal_iff]; exact subset.refl _) (@map_comap_le _ _ _ f)
id       └──────┘  └──────┘   └────────────────┘                 └─────────────┘  └──────────────┘         └─────────┘      └──────────┘       
src      └──────┘  └──────┘   └────────────────┘      └─────────┘└─────────────┘└┘└──────────────┘  └────┘└─────────┘└┘    └──────────┘
typ      └──────┘  └──────┘   └────────────────┘      └─────────┘└─────────────┘└┘└──────────────┘  └────┘└─────────┘└┘    └──────────┘       
doc                                                   └─────────┘               └┘                  └────┘           └┘
txt                                                   └─────────┘               └┘                  └────┘           └┘
par                                                   └─────────┘               └┘                  └────┘           └┘
pid                                                       └──┘└┘               └┘                                  └┘
st                                                   └─────────────────────────────────────────────────────────────────┘
557  
558  lemma mem_closure_of_tendsto {f : β → α} {b : filter β} {a : α} {s : set α}
id                                               └────┘               └─┘ 
src                                                └────┘                 └─┘
typ                                              └────┘               └─┘ 
559    (hb : b ≠ ⊥) (hf : tendsto f b (𝓝 a)) (h : f ⁻¹' s ∈ b) : a ∈ closure s :=
id                     └─────┘              └─┘         └─────┘ 
src                     └─────┘                  └─┘            └─────┘
typ                    └─────┘              └─┘         └─────┘ 
doc                       └─────┘                  └─┘              └─────┘
560  mem_of_closed_of_tendsto hb hf (is_closed_closure) $
id   └──────────────────────┘ └┘ └┘  └───────────────┘
src  └──────────────────────┘        └───────────────┘
typ  └──────────────────────┘ └┘ └┘  └───────────────┘
561    filter.mem_sets_of_superset h (preimage_mono subset_closure)
id     └─────────────────────────┘   └───────────┘ └────────────┘
src    └─────────────────────────┘    └───────────┘ └────────────┘
typ    └─────────────────────────┘   └───────────┘ └────────────┘
562  
563  /-- Suppose that `f` sends the complement to `s` to a single point `a`, and `l` is some filter.
564  Then `f` tends to `a` along `l` restricted to `s` if and only it tends to `a` along `l`. -/
565  lemma tendsto_inf_principal_nhds_iff_of_forall_eq {f : β → α} {l : filter β} {s : set β}
id                                                                    └────┘        └─┘ 
src                                                                     └────┘         └─┘
typ                                                                   └────┘        └─┘ 
566    {a : α} (h : ∀ x ∉ s, f x = a) :
id                           
src                             
typ                          
567    tendsto f (l ⊓ principal s) (𝓝 a) ↔ tendsto f l (𝓝 a) :=
id     └─────┘     └───────┘        └─────┘     
src    └─────┘       └───────┘          └─────┘      
typ    └─────┘     └───────┘        └─────┘     
doc    └─────┘        └───────┘           └─────┘      
568  begin
st   └─────
569    rw [tendsto_iff_comap, tendsto_iff_comap],
id         └───────────────┘  └───────────────┘
src    └──┘└───────────────┘└┘└───────────────┘
typ    └──┘└───────────────┘└┘└───────────────┘
doc    └──┘                 └┘                 
txt    └──┘                 └┘                 
par    └──┘                 └┘                 
pid      └┘                 └┘                 
st   ──────────────────────┘└─────────────────┘└──
570    replace h : principal (-s) ≤ comap f (𝓝 a),
id                 └───────┘     └───┘    
src    └──────────┘└───────┘  └┘└───┘   
typ    └──────────┘└───────┘ └┘└───┘ 
doc    └──────────┘└───────┘   └┘ └───┘   
txt    └──────────┘            └┘          
par    └──────────┘            └┘          
pid           └┘└─┘            └┘          
st   ───────────────────────────────────────────┘└─
571    { rintros U ⟨t, ht, htU⟩ x hx,
src      └─────────────────────────┘
typ      └─────────────────────────┘
doc      └─────────────────────────┘
txt      └─────────────────────────┘
par      └─────────────────────────┘
pid             └──────────────────┘
st   ───┘└─────────────────────────┘└─
572      have : f x ∈ t, from (h x hx).symm ▸ mem_of_nhds ht,
id                           └┘        └─────────┘ └┘
src      └─────┘     └───┘     └─────┘└─────────┘
typ      └─────┘  └───┘ └┘└─────┘└─────────┘└┘
doc      └─────┘      └───┘     └─────┘            
txt      └─────┘      └───┘     └─────┘            
par      └─────┘      └───┘     └─────┘            
pid      └───┘└┘      └───┘     └─────┘            
st   ─────────────────┘└───────────────────────────────────┘└─
573      exact htU this },
id             └─┘ └──┘
src      └────┘       
typ      └────┘└─┘└──┘
doc      └────┘       
txt      └────┘       
par      └────┘       
pid                  
st   ──────────────────┘└┘
574    refine ⟨λ h', _, le_trans inf_le_left⟩,
id                      └──────┘ └─────────┘
src    └─────┘  └──────┘└──────┘└─────────┘
typ    └─────┘  └──────┘└──────┘└─────────┘
doc    └─────┘  └──────┘                   
txt    └─────┘  └──────┘                   
par    └─────┘  └──────┘                   
pid            └──────┘                   
st   ───────────────────────────────────────┘└─
575    have := sup_le h' h,
id             └────┘ └┘ 
src    └──────┘└────┘  
typ    └──────┘└────┘└┘
doc    └──────┘        
txt    └──────┘        
par    └──────┘        
pid    └───┘└─┘        
st   ────────────────────┘└─
576    rw [sup_inf_right, sup_principal, union_compl_self, principal_univ,
id         └───────────┘  └───────────┘  └──────────────┘  └────────────┘
src    └──┘└───────────┘└┘└───────────┘└┘└──────────────┘└┘└────────────┘└─
typ    └──┘└───────────┘└┘└───────────┘└┘└──────────────┘└┘└────────────┘└─
doc    └──┘             └┘             └┘                └┘              └─
txt    └──┘             └┘             └┘                └┘              └─
par    └──┘             └┘             └┘                └┘              └─
pid      └┘             └┘             └┘                └┘              └─
st   ──────────────────┘└─────────────┘└────────────────┘└──────────────┘└─
577      inf_top_eq, sup_le_iff] at this,
id       └────────┘  └────────┘
src  ───┘└────────┘└┘└────────┘└───────┘
typ  ───┘└────────┘└┘└────────┘└───────┘
doc  ───┘          └┘          └───────┘
txt  ───┘          └┘          └───────┘
par  ───┘          └┘          └───────┘
pid  ───┘          └┘          └──────┘
st   ─────────────┘└──────────┘└──────┘└─
578    exact this.1
id           └──┘
src    └────┘    └─┘
typ    └────┘└──┘└─┘
doc    └────┘    └─┘
txt    └────┘    └─┘
par    └────┘    └─┘
pid             └─┘
st   ──────────────┘
579  end
st   └─┘
580  
581  section lim
582  variables [inhabited α]
id              └───────┘
src             └───────┘
typ             └───────┘
583  
584  /-- If `f` is a filter, then `lim f` is a limit of the filter, if it exists. -/
585  noncomputable def lim (f : filter α) : α := epsilon $ λa, f ≤ 𝓝 a
id                              └────┘         └─────┘         
src                             └────┘           └─────┘          
typ                             └────┘         └─────┘         
doc                                                                
586  
587  lemma lim_spec {f : filter α} (h : ∃a, f ≤ 𝓝 a) : f ≤ 𝓝 (lim f) := epsilon_spec h
id                       └────┘                    └─┘      └──────────┘ 
src                      └────┘                         └─┘       └──────────┘
typ                      └────┘                    └─┘      └──────────┘ 
doc                                                         └─┘
588  end lim
589  
590  
591  /- locally finite family [General Topology (Bourbaki, 1995)] -/
592  section locally_finite
593  
594  /-- A family of sets in `set α` is locally finite if at every point `x:α`,
595    there is a neighborhood of `x` which meets only finitely many sets in the family -/
596  def locally_finite (f : β → set α) :=
id                              └─┘ 
src                              └─┘
typ                             └─┘ 
597  ∀x:α, ∃t ∈ 𝓝 x, finite {i | (f i ∩ t).nonempty }
id             └────┘         └──────┘
src               └────┘             └──────┘
typ            └────┘         └──────┘
doc                 └────┘               └──────┘
598  
599  lemma locally_finite_of_finite {f : β → set α} (h : finite (univ : set β)) : locally_finite f :=
id                                          └─┘        └────┘  └──┘   └─┘      └────────────┘ 
src                                          └─┘         └────┘  └──┘   └─┘       └────────────┘
typ                                         └─┘        └────┘  └──┘   └─┘      └────────────┘ 
doc                                                      └────┘                   └────────────┘
600  assume x, ⟨univ, univ_mem_sets, finite_subset h $ subset_univ _⟩
id             └──┘  └───────────┘  └───────────┘    └─────────┘
src             └──┘  └───────────┘  └───────────┘     └─────────┘
typ            └──┘  └───────────┘  └───────────┘    └─────────┘
601  
602  lemma locally_finite_subset
603    {f₁ f₂ : β → set α} (hf₂ : locally_finite f₂) (hf : ∀b, f₁ b ⊆ f₂ b) : locally_finite f₁ :=
id                 └─┘          └────────────┘ └┘           └┘   └┘     └────────────┘ └┘
src                 └─┘           └────────────┘                             └────────────┘
typ                └─┘          └────────────┘ └┘           └┘   └┘     └────────────┘ └┘
doc                               └────────────┘                              └────────────┘
604  assume a,
id          
typ         
605  let ⟨t, ht₁, ht₂⟩ := hf₂ a in
id   └─┘    └─┘  └─┘     └─┘ 
typ  └─┘    └─┘  └─┘     └─┘ 
606  ⟨t, ht₁, finite_subset ht₂ $ assume i hi,
id            └───────────┘               └┘
src           └───────────┘
typ           └───────────┘               └┘
607     hi.mono $ inter_subset_inter (hf i) $ subset.refl _⟩
id      └┘└───┘   └────────────────┘  └┘     └─────────┘
src       └───┘   └────────────────┘          └─────────┘
typ     └┘└───┘   └────────────────┘  └┘     └─────────┘
608  
609  lemma is_closed_Union_of_locally_finite {f : β → set α}
id                                                   └─┘ 
src                                                   └─┘
typ                                                  └─┘ 
610    (h₁ : locally_finite f) (h₂ : ∀i, is_closed (f i)) : is_closed (⋃i, f i) :=
id           └────────────┘            └───────┘        └───────┘    
src          └────────────┘              └───────┘          └───────┘   
typ          └────────────┘            └───────┘        └───────┘    
doc          └────────────┘              └───────┘          └───────┘   
611  is_open_iff_nhds.mpr $ assume a, assume h : a ∉ (⋃i, f i),
id   └──────────────┘└──┘                            
src  └──────────────┘└──┘                             
typ  └──────────────┘└──┘                            
doc                                                    
612    have ∀i, a ∈ -f i,
id                
src                
typ               
613      from assume i hi, h $ mem_Union.2 ⟨i, hi⟩,
id                    └┘     └───────┘     └┘
src                            └───────┘
typ                   └┘     └───────┘     └┘
614    have ∀i, - f i ∈ (𝓝 a).sets,
id                    └──┘
src                       └──┘
typ                   └──┘
doc                      
615      by rw [nhds_sets]; exact assume i, ⟨- f i, subset.refl _, h₂ i, this i⟩,
id              └───────┘                         └─────────┘    └┘    └──┘
src         └──┘└───────┘  └────┘      └──┘   └┘└─────────┘└──┘   └┘     
typ         └──┘└───────┘  └────┘      └──┘  └┘└─────────┘└──┘└┘ └┘└──┘ 
doc         └──┘           └────┘      └──┘    └┘           └──┘   └┘     
txt         └──┘           └────┘      └──┘    └┘           └──┘   └┘     
par         └──┘           └────┘      └──┘    └┘           └──┘   └┘     
pid           └┘                      └──┘    └┘           └──┘   └┘     
st         └────────────┘└────────────────────────────────────────────────────┘
616    let ⟨t, h_sets, (h_fin : finite {i | (f i ∩ t).nonempty })⟩ := h₁ a in
id     └─┘                     └────┘          └──────┘         └┘ 
src                             └────┘             └──────┘
typ    └─┘                     └────┘          └──────┘         └┘ 
doc                             └────┘               └──────┘
617  
618    calc 𝓝 a ≤ principal (t ∩ (⋂ i∈{i | (f i ∩ t).nonempty }, - f i)) :
id              └───────┘                 └──────┘      
src              └───────┘                     └──────┘    
typ             └───────┘                 └──────┘      
doc              └───────┘                        └──────┘   
619    begin
st     └─────
620      rw [le_principal_iff],
id           └──────────────┘
src      └──┘└──────────────┘
typ      └──┘└──────────────┘
doc      └──┘                
txt      └──┘                
par      └──┘                
pid        └┘                
st   ───────────────────────┘└──
621      apply @filter.inter_mem_sets _ (𝓝 a) _ _ h_sets,
id              └───────────────────┘           └────┘
src      └────┘ └───────────────────┘└─┘  └────┘
typ      └────┘ └───────────────────┘└─┘ └────┘└────┘
doc      └────┘                      └─┘  └────┘
txt      └────┘                      └─┘   └────┘
par      └────┘                      └─┘   └────┘
pid                                 └─┘   └────┘
st   ──────────────────────────────────────────────────┘└─
622      apply @filter.Inter_mem_sets _ (𝓝 a) _ _ _ h_fin,
id              └───────────────────┘              └───┘
src      └────┘ └───────────────────┘└─┘   └──────┘
typ      └────┘ └───────────────────┘└─┘  └──────┘└───┘
doc      └────┘                      └─┘   └──────┘
txt      └────┘                      └─┘   └──────┘
par      └────┘                      └─┘   └──────┘
pid                                 └─┘   └──────┘
st   ───────────────────────────────────────────────────┘└─
623      exact assume i h, this i
id                         └──┘
src      └────┘      └────┘     
typ      └────┘      └────┘└──┘ 
doc      └────┘      └────┘     
txt      └────┘      └────┘     
par      └────┘      └────┘     
pid                 └────┘     
st   ─────────────────────────────
624    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
625    ... ≤ principal (- ⋃i, f i) :
id           └───────┘     
src          └───────┘    
typ          └───────┘     
doc          └───────┘     
626    begin
st     └─────
627      simp only [principal_mono, subset_def, mem_compl_eq, mem_inter_eq,
id                  └────────────┘  └────────┘  └──────────┘  └──────────┘
src      └─────────┘└────────────┘└┘└────────┘└┘└──────────┘└┘└──────────┘└─
typ      └─────────┘└────────────┘└┘└────────┘└┘└──────────┘└┘└──────────┘└─
doc      └─────────┘              └┘          └┘            └┘            └─
txt      └─────────┘              └┘          └┘            └┘            └─
par      └─────────┘              └┘          └┘            └┘            └─
pid          └──┘└┘              └┘          └┘            └┘            └─
st   ───────────────────────────────────────────────────────────────────────
628        mem_Inter, mem_set_of_eq, mem_Union, and_imp, not_exists,
id         └───────┘  └───────────┘  └───────┘  └─────┘  └────────┘
src  ─────┘└───────┘└┘└───────────┘└┘└───────┘└┘└─────┘└┘└────────┘└─
typ  ─────┘└───────┘└┘└───────────┘└┘└───────┘└┘└─────┘└┘└────────┘└─
doc  ─────┘         └┘             └┘         └┘       └┘          └─
txt  ─────┘         └┘             └┘         └┘       └┘          └─
par  ─────┘         └┘             └┘         └┘       └┘          └─
pid  ─────┘         └┘             └┘         └┘       └┘          └─
st   ────────────────────────────────────────────────────────────────
629        exists_imp_distrib, ne_empty_iff_nonempty, set.nonempty],
id         └────────────────┘  └───────────────────┘  └──────────┘
src  ─────┘└────────────────┘└┘└───────────────────┘└┘└──────────┘
typ  ─────┘└────────────────┘└┘└───────────────────┘└┘└──────────┘
doc  ─────┘                  └┘                     └┘└──────────┘
txt  ─────┘                  └┘                     └┘            
par  ─────┘                  └┘                     └┘            
pid  ─────┘                  └┘                     └┘            
st   ─────────────────────────────────────────────────────────────┘└─
630      exact assume x xt ht i xfi, ht i x xfi xt xfi
src      └────┘      └──────────────┘            
typ      └────┘      └──────────────┘            
doc      └────┘      └──────────────┘            
txt      └────┘      └──────────────┘            
par      └────┘      └──────────────┘            
pid                 └──────────────┘            
st   ──────────────────────────────────────────────────
631    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
632  
633  end locally_finite
634  
635  end topological_space
636  
637  section continuous
638  variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
id             
typ            
639  variables [topological_space α] [topological_space β] [topological_space γ]
id              └───────────────┘     └───────────────┘     └───────────────┘
src             └───────────────┘     └───────────────┘     └───────────────┘
typ             └───────────────┘     └───────────────┘     └───────────────┘
doc             └───────────────┘     └───────────────┘     └───────────────┘
640  open_locale topological_space
641  
642  /-- A function between topological spaces is continuous if the preimage
643    of every open set is open. -/
644  def continuous (f : α → β) := ∀s, is_open s → is_open (f ⁻¹' s)
id                                  └─────┘    └─────┘   └─┘ 
src                                    └─────┘     └─────┘    └─┘
typ                                 └─────┘    └─────┘   └─┘ 
doc                                    └─────┘     └─────┘    └─┘
645  
646  /-- A function between topological spaces is continuous at a point `x₀`
647  if `f x` tends to `f x₀` when `x` tends to `x₀`. -/
648  def continuous_at (f : α → β) (x : α) := tendsto f (𝓝 x) (𝓝 (f x))
id                                         └─────┘          
src                                           └─────┘         
typ                                        └─────┘          
doc                                           └─────┘         
649  
650  lemma continuous_at.preimage_mem_nhds {f : α → β} {x : α} {t : set β} (h : continuous_at f x)
id                                                               └─┘        └───────────┘  
src                                                                 └─┘         └───────────┘
typ                                                              └─┘        └───────────┘  
doc                                                                             └───────────┘
651    (ht : t ∈ 𝓝 (f x)) : f ⁻¹' t ∈ 𝓝 x :=
id                      └─┘    
src                         └─┘    
typ                     └─┘    
doc                          └─┘     
652  h ht
id    └┘
typ   └┘
653  
654  lemma continuous_id : continuous (id : α → α) :=
id                         └────────┘  └┘      
src                        └────────┘  └┘
typ                        └────────┘  └┘      
doc                        └────────┘
655  assume s h, h
id             
typ            
656  
657  lemma continuous.comp {g : β → γ} {f : α → β} (hg : continuous g) (hf : continuous f) :
id                                                   └────────┘         └────────┘ 
src                                                      └────────┘          └────────┘
typ                                                  └────────┘         └────────┘ 
doc                                                      └────────┘          └────────┘
658    continuous (g ∘ f) :=
id     └────────┘    
src    └────────┘    
typ    └────────┘    
doc    └────────┘
659  assume s h, hf _ (hg s h)
id             └┘    └┘  
typ            └┘    └┘  
660  
661  lemma continuous_at.comp {g : β → γ} {f : α → β} {x : α}
id                                                     
typ                                                    
662    (hg : continuous_at g (f x)) (hf : continuous_at f x) :
id           └───────────┘             └───────────┘  
src          └───────────┘                └───────────┘
typ          └───────────┘             └───────────┘  
doc          └───────────┘                └───────────┘
663    continuous_at (g ∘ f) x :=
id     └───────────┘      
src    └───────────┘    
typ    └───────────┘      
doc    └───────────┘
664  hg.comp hf
id   └┘└───┘ └┘
src    └───┘
typ  └┘└───┘ └┘
665  
666  lemma continuous.tendsto {f : α → β} (hf : continuous f) (x) :
id                                            └────────┘ 
src                                             └────────┘
typ                                           └────────┘ 
doc                                             └────────┘
667    tendsto f (𝓝 x) (𝓝 (f x)) | s :=
id     └─────┘               
src    └─────┘         
typ    └─────┘               
doc    └─────┘         
668  show s ∈ 𝓝 (f x) → s ∈ map f (𝓝 x),
id                    └─┘    
src                      └─┘    
typ                   └─┘    
doc                        └─┘    
669  by simp [nhds_sets]; exact
id            └───────┘
src     └────┘└───────┘  └────┘
typ     └────┘└───────┘  └────┘
doc     └────┘           └────┘
txt     └────┘           └────┘
par     └────┘           └────┘
pid                         
st     └────────────────────────
670  assume t t_subset t_open fx_in_t,
src        └───────────────────────────
typ        └───────────────────────────
doc        └───────────────────────────
txt        └───────────────────────────
par        └───────────────────────────
pid        └───────────────────────────
st   ──────────────────────────────────
671    ⟨f ⁻¹' t, preimage_mono t_subset, hf t t_open, fx_in_t⟩
id       └─┘    └───────────┘           └┘
src  ─┘  └─┘ └┘└───────────┘        └┘         └┘       └─
typ  ─┘ └─┘ └┘└───────────┘        └┘└┘       └┘       └─
doc  ─┘  └─┘ └┘                     └┘         └┘       └─
txt  ─┘      └┘                     └┘         └┘       └─
par  ─┘      └┘                     └┘         └┘       └─
pid  ─┘      └┘                     └┘         └┘       
st   ──────────────────────────────────────────────────────────
672  
src  
typ  
doc  
txt  
par  
pid  
st   
673  lemma continuous.continuous_at {f : α → β} {x : α} (h : continuous f) :
id                                                        └────────┘ 
src                                                          └────────┘
typ                                                       └────────┘ 
doc                                                          └────────┘
674    continuous_at f x :=
id     └───────────┘  
src    └───────────┘
typ    └───────────┘  
doc    └───────────┘
675  h.tendsto x
id   └──────┘ 
src   └──────┘
typ  └──────┘ 
676  
677  lemma continuous_iff_continuous_at {f : α → β} : continuous f ↔ ∀ x, continuous_at f x :=
id                                                  └────────┘       └───────────┘  
src                                                   └────────┘         └───────────┘
typ                                                 └────────┘       └───────────┘  
doc                                                   └────────┘          └───────────┘
678  ⟨continuous.tendsto,
id    └────────────────┘
src   └────────────────┘
typ   └────────────────┘
679    assume hf : ∀x, tendsto f (𝓝 x) (𝓝 (f x)),
id                    └─────┘          
src                    └─────┘         
typ                   └─────┘          
doc                    └─────┘         
680    assume s, assume hs : is_open s,
id                          └─────┘ 
src                          └─────┘
typ                         └─────┘ 
doc                          └─────┘
681    have ∀a, f a ∈ s → s ∈ 𝓝 (f a),
id                        
src                         
typ                       
doc                           
682      by simp [nhds_sets]; exact assume a ha, ⟨s, subset.refl s, hs, ha⟩,
id                └───────┘                          └─────────┘   └┘
src         └────┘└───────┘  └────┘      └─────┘  └┘└─────────┘ └┘  └┘  
typ         └────┘└───────┘  └────┘      └─────┘  └┘└─────────┘└┘└┘└┘  
doc         └────┘           └────┘      └─────┘  └┘            └┘  └┘  
txt         └────┘           └────┘      └─────┘  └┘            └┘  └┘  
par         └────┘           └────┘      └─────┘  └┘            └┘  └┘  
pid                                   └─────┘  └┘            └┘  └┘  
st         └──────────────────────────────────────────────────────────────┘
683    show is_open (f ⁻¹' s),
id          └─────┘   └─┘ 
src         └─────┘    └─┘
typ         └─────┘   └─┘ 
doc         └─────┘    └─┘
684      by simp [is_open_iff_nhds]; exact assume a ha, hf a (this a ha)⟩
id                └──────────────┘                      └┘    └──┘
src         └────┘└──────────────┘  └────┘      └─────┘           
typ         └────┘└──────────────┘  └────┘      └─────┘└┘  └──┘   
doc         └────┘                  └────┘      └─────┘           
txt         └────┘                  └────┘      └─────┘           
par         └────┘                  └────┘      └─────┘           
pid                                          └─────┘           
st         └───────────────────────────────────────────────────────────┘
685  
686  lemma continuous_const {b : β} : continuous (λa:α, b) :=
id                                   └────────┘       
src                                   └────────┘
typ                                  └────────┘       
doc                                   └────────┘
687  continuous_iff_continuous_at.mpr $ assume a, tendsto_const_nhds
id   └──────────────────────────┘└──┘            └────────────────┘
src  └──────────────────────────┘└──┘             └────────────────┘
typ  └──────────────────────────┘└──┘            └────────────────┘
688  
689  lemma continuous_at_const {x : α} {b : β} : continuous_at (λ a:α, b) x :=
id                                             └───────────┘          
src                                              └───────────┘
typ                                            └───────────┘          
doc                                              └───────────┘
690  continuous_const.continuous_at
id   └──────────────┘└────────────┘
src  └──────────────┘└────────────┘
typ  └──────────────┘└────────────┘
691  
692  lemma continuous_at_id {x : α} : continuous_at id x :=
id                                   └───────────┘ └┘ 
src                                   └───────────┘ └┘
typ                                  └───────────┘ └┘ 
doc                                   └───────────┘
693  continuous_id.continuous_at
id   └───────────┘└────────────┘
src  └───────────┘└────────────┘
typ  └───────────┘└────────────┘
694  
695  lemma continuous_iff_is_closed {f : α → β} :
id                                          
typ                                         
696    continuous f ↔ (∀s, is_closed s → is_closed (f ⁻¹' s)) :=
id     └────────┘       └───────┘    └───────┘   └─┘ 
src    └────────┘         └───────┘     └───────┘    └─┘
typ    └────────┘       └───────┘    └───────┘   └─┘ 
doc    └────────┘          └───────┘     └───────┘    └─┘
697  ⟨assume hf s hs, hf (-s) hs,
id           └┘  └┘  └┘    └┘
src                       
typ          └┘  └┘  └┘    └┘
698    assume hf s, by rw [←is_closed_compl_iff, ←is_closed_compl_iff]; exact hf _⟩
id            └┘           └─────────────────┘   └─────────────────┘         └┘
src                    └───┘└─────────────────┘└─┘└─────────────────┘  └────┘  └┘
typ           └┘      └───┘└─────────────────┘└─┘└─────────────────┘  └────┘└┘└┘
doc                    └───┘                   └─┘                     └────┘  └┘
txt                    └───┘                   └─┘                     └────┘  └┘
par                    └───┘                   └─┘                     └────┘  └┘
pid                      └─┘                   └─┘                            └┘
st                    └───────────────────────┘└────────────────────┘└──────────┘
699  
700  lemma continuous_at_iff_ultrafilter {f : α → β} (x) : continuous_at f x ↔
id                                                       └───────────┘   
src                                                        └───────────┘     
typ                                                      └───────────┘   
doc                                                        └───────────┘
701    ∀ g, is_ultrafilter g → g ≤ 𝓝 x → g.map f ≤ 𝓝 (f x) :=
id         └────────────┘          └──┘      
src         └────────────┘              └──┘    
typ        └────────────┘          └──┘      
doc         └────────────┘               └──┘     
702  tendsto_iff_ultrafilter f (𝓝 x) (𝓝 (f x))
id   └─────────────────────┘          
src  └─────────────────────┘         
typ  └─────────────────────┘          
doc  └─────────────────────┘         
703  
704  lemma continuous_iff_ultrafilter {f : α → β} :
id                                            
typ                                           
705    continuous f ↔ ∀ x g, is_ultrafilter g → g ≤ 𝓝 x → g.map f ≤ 𝓝 (f x) :=
id     └────────┘        └────────────┘          └──┘      
src    └────────┘           └────────────┘              └──┘    
typ    └────────┘        └────────────┘          └──┘      
doc    └────────┘            └────────────┘               └──┘     
706  by simp only [continuous_iff_continuous_at, continuous_at_iff_ultrafilter]
id                 └──────────────────────────┘  └───────────────────────────┘
src     └─────────┘└──────────────────────────┘└┘└───────────────────────────┘└─
typ     └─────────┘└──────────────────────────┘└┘└───────────────────────────┘└─
doc     └─────────┘                            └┘                             └─
txt     └─────────┘                            └┘                             └─
par     └─────────┘                            └┘                             └─
pid         └──┘└┘                            └┘                             
st     └────────────────────────────────────────────────────────────────────────
707  
src  
typ  
doc  
txt  
par  
pid  
st   
708  /-- A piecewise defined function `if p then f else g` is continuous, if both `f` and `g`
709  are continuous, and they coincide on the frontier (boundary) of the set `{a | p a}`. -/
710  lemma continuous_if {p : α → Prop} {f g : α → β} {h : ∀a, decidable (p a)}
id                                                         └───────┘   
src                                                            └───────┘
typ                                                        └───────┘   
711    (hp : ∀a∈frontier {a | p a}, f a = g a) (hf : continuous f) (hg : continuous g) :
id             └──────┘                    └────────┘         └────────┘ 
src             └──────┘                           └────────┘          └────────┘
typ            └──────┘                    └────────┘         └────────┘ 
doc             └──────┘                             └────────┘          └────────┘
712    continuous (λa, @ite (p a) (h a) β (f a) (g a)) :=
id     └────────┘      └─┘                
src    └────────┘       └─┘
typ    └────────┘      └─┘                
doc    └────────┘
713  continuous_iff_is_closed.mpr $
id   └──────────────────────┘└──┘
src  └──────────────────────┘└──┘
typ  └──────────────────────┘└──┘
714  assume s hs,
id           └┘
typ          └┘
715  have (λa, ite (p a) (f a) (g a)) ⁻¹' s =
id            └─┘              └─┘  
src            └─┘                    └─┘   
typ           └─┘              └─┘  
doc                                   └─┘
716      (closure {a | p a} ∩  f ⁻¹' s) ∪ (closure {a | ¬ p a} ∩ g ⁻¹' s),
id        └─────┘          └─┘     └─────┘          └─┘ 
src       └─────┘              └─┘      └─────┘              └─┘
typ       └─────┘          └─┘     └─────┘          └─┘ 
doc       └─────┘                └─┘       └─────┘                 └─┘
717    from set.ext $ assume a,
id          └─────┘          
src         └─────┘
typ         └─────┘          
718    classical.by_cases
id     └────────────────┘
src    └────────────────┘
typ    └────────────────┘
719      (assume : a ∈ frontier {a | p a},
id                   └──────┘     
src                   └──────┘ 
typ                  └──────┘     
doc                    └──────┘
720        have hac : a ∈ closure {a | p a}, from this.left,
id                      └─────┘             └──┘└───┘
src                      └─────┘                    └───┘
typ                     └─────┘             └──┘└───┘
doc                       └─────┘
721        have hai : a ∈ closure {a | ¬ p a},
id                      └─────┘      
src                      └─────┘     
typ                     └─────┘      
doc                       └─────┘
722          from have a ∈ - interior {a | p a}, from this.right, by rwa [←closure_compl] at this,
id                        └──────┘             └──┘└────┘           └───────────┘
src                        └──────┘                    └────┘     └────┘└───────────┘└───────┘
typ                       └──────┘             └──┘└────┘     └────┘└───────────┘└───────┘
doc                          └──────┘                                └────┘             └───────┘
txt                                                                  └────┘             └───────┘
par                                                                  └────┘             └───────┘
pid                                                                     └─┘             └──────┘
st                                                                  └──────────────────┘└──────┘
723        by by_cases p a; simp [h, hp a this, hac, hai, iff_def] {contextual := tt})
id                                └┘  └──┘  └─┘  └─┘  └─────┘                 └┘
src           └───────┘    └────┘ └┘       └┘   └┘   └┘└─────┘└┘ └────────────┘└┘
typ           └───────┘  └────┘└┘└┘└──┘└┘└─┘└┘└─┘└┘└─────┘└┘ └────────────┘└┘
doc           └───────┘    └────┘ └┘       └┘   └┘   └┘       └┘ └────────────┘  
txt           └───────┘    └────┘ └┘       └┘   └┘   └┘       └┘ └────────────┘  
par           └───────┘    └────┘ └┘       └┘   └┘   └┘       └┘ └────────────┘  
pid                            └┘       └┘   └┘   └┘        └────────────┘  
st           └──────────────────────────────────────────────────────────────────────┘
724      (assume hf : a ∈ - frontier {a | p a},
id                       └──────┘     
src                       └──────┘ 
typ                      └──────┘     
doc                         └──────┘
725        classical.by_cases
id         └────────────────┘
src        └────────────────┘
typ        └────────────────┘
726          (assume : p a,
id                      
typ                     
727            have hc : a ∈ closure {a | p a}, from subset_closure this,
id                         └─────┘             └────────────┘ └──┘
src                         └─────┘                └────────────┘
typ                        └─────┘             └────────────┘ └──┘
doc                          └─────┘
728            have hnc : a ∉ closure {a | ¬ p a},
id                          └─────┘      
src                          └─────┘     
typ                         └─────┘      
doc                           └─────┘
729              by show a ∉ closure (- {a | p a}); rw [closure_compl]; simpa [frontier, hc] using hf,
id                         └─────┘                 └───────────┘          └──────┘  └┘        └┘
src                 └───┘ └─────┘ └──┘  └┘  └──┘└───────────┘  └─────┘└──────┘└┘  └──────┘
typ                 └───┘└─────┘ └──┘ └┘  └──┘└───────────┘  └─────┘└──────┘└┘└┘└──────┘└┘
doc                 └───┘  └─────┘   └──┘  └┘  └──┘               └─────┘└──────┘└┘  └──────┘
txt                 └───┘            └──┘  └┘  └──┘               └─────┘        └┘  └──────┘
par                 └───┘            └──┘  └┘  └──┘               └─────┘        └┘  └──────┘
pid                 └───┘            └──┘  └┘    └┘                            └┘  └────┘
st                 └───────────────────────────────────┘└───────────┘└─────────────────────────────┘
730            by simp [this, hc, hnc])
id                      └──┘  └┘  └─┘
src               └────┘    └┘  └┘   
typ               └────┘└──┘└┘└┘└┘└─┘
doc               └────┘    └┘  └┘   
txt               └────┘    └┘  └┘   
par               └────┘    └┘  └┘   
pid                       └┘  └┘   
st               └───────────────────┘
731          (assume : ¬ p a,
id                       
src                    
typ                      
732            have hc : a ∈ closure {a | ¬ p a}, from subset_closure this,
id                         └─────┘              └────────────┘ └──┘
src                         └─────┘                 └────────────┘
typ                        └─────┘              └────────────┘ └──┘
doc                          └─────┘
733            have hnc : a ∉ closure {a | p a},
id                          └─────┘     
src                          └─────┘ 
typ                         └─────┘     
doc                           └─────┘
734              begin
st               └─────
735                have hc : a ∈ closure (- {a | p a}), from hc,
id                              └─────┘                   └┘
src                └────────┘  └─────┘  └──┘  └┘  └───┘
typ                └────────┘ └─────┘  └──┘ └┘  └───┘└┘
doc                └────────┘  └─────┘   └──┘  └┘  └───┘
txt                └────────┘            └──┘  └┘  └───┘
par                └────────┘            └──┘  └┘  └───┘
pid                └─────┘└─┘            └──┘  └┘  └───┘
st   ────────────────────────────────────────────────┘└───────┘└─
736                simp [closure_compl] at hc,
id                       └───────────┘
src                └────┘└───────────┘└─────┘
typ                └────┘└───────────┘└─────┘
doc                └────┘             └─────┘
txt                └────┘             └─────┘
par                └────┘             └─────┘
pid                                 └───┘
st   ───────────────────────────────────────┘└─
737                simpa [frontier, hc] using hf
id                        └──────┘  └┘        └┘
src                └─────┘└──────┘└┘  └──────┘  
typ                └─────┘└──────┘└┘└┘└──────┘└┘
doc                └─────┘└──────┘└┘  └──────┘  
txt                └─────┘        └┘  └──────┘  
par                └─────┘        └┘  └──────┘  
pid                             └┘  └────┘  
st   ────────────────────────────────────────────
738              end,
src  ───────────┘
typ  ───────────┘
doc  ───────────┘
txt  ───────────┘
par  ───────────┘
pid  ───────────┘
st   ───────────┘└─┘
739            by simp [this, hc, hnc])),
id                      └──┘  └┘  └─┘
src               └────┘    └┘  └┘   
typ               └────┘└──┘└┘└┘└┘└─┘
doc               └────┘    └┘  └┘   
txt               └────┘    └┘  └┘   
par               └────┘    └┘  └┘   
pid                       └┘  └┘   
st               └───────────────────┘
740  by rw [this]; exact is_closed_union
id          └──┘         └─────────────┘
src     └──┘      └────┘└─────────────┘
typ     └──┘└──┘  └────┘└─────────────┘
doc     └──┘      └────┘               
txt     └──┘      └────┘               
par     └──┘      └────┘               
pid       └┘                          
st     └───────┘└───────────────────────
741    (is_closed_inter is_closed_closure $ continuous_iff_is_closed.mp hf s hs)
id                                                                      └┘
src  ─┘                                                                  └─
typ  ─┘                                                             └┘   └─
doc  ─┘                                                                  └─
txt  ─┘                                                                  └─
par  ─┘                                                                  └─
pid  ─┘                                                                  └─
st   ────────────────────────────────────────────────────────────────────────────
742    (is_closed_inter is_closed_closure $ continuous_iff_is_closed.mp hg s hs)
id      └─────────────┘ └───────────────┘   └─────────────────────────┘ └┘  └┘
src  ─┘ └─────────────┘└───────────────┘ └─────────────────────────┘     └─
typ  ─┘ └─────────────┘└───────────────┘ └─────────────────────────┘└┘└┘└─
doc  ─┘                                                                  └─
txt  ─┘                                                                  └─
par  ─┘                                                                  └─
pid  ─┘                                                                  
st   ────────────────────────────────────────────────────────────────────────────
743  
src  
typ  
doc  
txt  
par  
pid  
st   
744  
src  
typ  
doc  
txt  
par  
pid  
st   
745  /- Continuity and partial functions -/
src  ───────────────────────────────────────
typ  ───────────────────────────────────────
doc  ───────────────────────────────────────
txt  ───────────────────────────────────────
par  ───────────────────────────────────────
pid  ───────────────────────────────────────
st   ───────────────────────────────────────
746  
src  
typ  
doc  
txt  
par  
pid  
st   
747  /-- Continuity of a partial function -/
748  def pcontinuous (f : α →. β) := ∀ s, is_open s → is_open (f.preimage s)
id                         └┘          └─────┘    └─────┘  └───────┘ 
src                         └┘            └─────┘     └─────┘   └───────┘
typ                        └┘          └─────┘    └─────┘  └───────┘ 
doc                         └┘            └─────┘     └─────┘
749  
750  lemma open_dom_of_pcontinuous {f : α →. β} (h : pcontinuous f) : is_open f.dom :=
id                                       └┘        └─────────┘     └─────┘ └──┘
src                                       └┘         └─────────┘      └─────┘  └──┘
typ                                      └┘        └─────────┘     └─────┘ └──┘
doc                                       └┘         └─────────┘      └─────┘  └──┘
751  by rw [←pfun.preimage_univ]; exact h _ is_open_univ
id           └────────────────┘            └──────────┘
src     └───┘└────────────────┘  └────┘ └─┘└──────────┘
typ     └───┘└────────────────┘  └────┘└─┘└──────────┘
doc     └───┘                    └────┘ └─┘            
txt     └───┘                    └────┘ └─┘            
par     └───┘                    └────┘ └─┘            
pid       └─┘                          └─┘            
st     └──────────────────────┘└────────────────────────
752  
src  
typ  
doc  
txt  
par  
pid  
st   
753  lemma pcontinuous_iff' {f : α →. β} :
id                                └┘ 
src                                └┘
typ                               └┘ 
doc                                └┘
754    pcontinuous f ↔ ∀ {x y} (h : y ∈ f x), ptendsto' f (𝓝 x) (𝓝 y) :=
id     └─────────┘                    └───────┘        
src    └─────────┘                          └───────┘         
typ    └─────────┘                    └───────┘        
doc    └─────────┘                                              
755  begin
st   └─────
756    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
757    { intros h x y h',
src      └─────────────┘
typ      └─────────────┘
doc      └─────────────┘
txt      └─────────────┘
par      └─────────────┘
pid            └───────┘
st   ───┘└─────────────┘└─
758      rw [ptendsto'_def],
id           └───────────┘
src      └──┘└───────────┘
typ      └──┘└───────────┘
doc      └──┘             
txt      └──┘             
par      └──┘             
pid        └┘             
st   ────────────────────┘└──
759      change ∀ (s : set β), s ∈ (𝓝 y).sets → pfun.preimage f s ∈ (𝓝 x).sets,
id                     └─┘                  └───────────┘         
src      └─────┘ └────┘└─┘     └─────┘ └───────────┘      └────┘
typ      └─────┘ └────┘└─┘   └─────┘ └───────────┘    └────┘
doc      └─────┘ └────┘         └─────┘                    └────┘
txt      └─────┘ └────┘          └─────┘                    └────┘
par      └─────┘ └────┘          └─────┘                    └────┘
pid             └────┘          └─────┘                    └───┘
st   ────────────────────────────────────────────────────────────────────────┘└─
760      rw [nhds_sets, nhds_sets],
id           └───────┘  └───────┘
src      └──┘└───────┘└┘└───────┘
typ      └──┘└───────┘└┘└───────┘
doc      └──┘         └┘         
txt      └──┘         └┘         
par      └──┘         └┘         
pid        └┘         └┘         
st   ────────────────┘└─────────┘└──
761      rintros s ⟨t, tsubs, opent, yt⟩,
src      └─────────────────────────────┘
typ      └─────────────────────────────┘
doc      └─────────────────────────────┘
txt      └─────────────────────────────┘
par      └─────────────────────────────┘
pid             └──────────────────────┘
st   ──────────────────────────────────┘└─
762      exact ⟨f.preimage t, pfun.preimage_mono _ tsubs, h _ opent, ⟨y, yt, h'⟩⟩
id              └────────┘   └────────────────┘   └───┘     └───┘     └┘  └┘
src      └────┘ └────────┘ └┘└────────────────┘└─┘     └┘ └─┘     └┘  └┘  └┘  └──
typ      └────┘ └────────┘└┘└────────────────┘└─┘└───┘└┘└─┘└───┘└┘ └┘└┘└┘└┘└──
doc      └────┘            └┘                  └─┘     └┘ └─┘     └┘  └┘  └┘  └──
txt      └────┘            └┘                  └─┘     └┘ └─┘     └┘  └┘  └┘  └──
par      └────┘            └┘                  └─┘     └┘ └─┘     └┘  └┘  └┘  └──
pid                       └┘                  └─┘     └┘ └─┘     └┘  └┘  └┘  └┘
st   ─────────────────────────────────────────────────────────────────────────────
763    },
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└┘
764    intros hf s os,
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid          └──────┘
st   ───────────────┘└─
765    rw is_open_iff_nhds,
id        └──────────────┘
src    └─┘└──────────────┘
typ    └─┘└──────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────────────────┘└─
766    rintros x ⟨y, ys, fxy⟩ t,
src    └──────────────────────┘
typ    └──────────────────────┘
doc    └──────────────────────┘
txt    └──────────────────────┘
par    └──────────────────────┘
pid           └───────────────┘
st   ─────────────────────────┘└─
767    rw [mem_principal_sets],
id         └────────────────┘
src    └──┘└────────────────┘
typ    └──┘└────────────────┘
doc    └──┘                  
txt    └──┘                  
par    └──┘                  
pid      └┘                  
st   ───────────────────────┘└──
768    assume h : f.preimage s ⊆ t,
id                └────────┘   
src    └─────────┘└────────┘ 
typ    └─────────┘└────────┘
doc    └─────────┘            
txt    └─────────┘            
par    └─────────┘            
pid    └─────────┘            
st   ────────────────────────────┘└─
769    change t ∈ 𝓝 x,
id                 
src    └─────┘   
typ    └─────┘  
doc    └─────┘   
txt    └─────┘   
par    └─────┘   
pid             
st   ──────────────────
770    apply mem_sets_of_superset _ h,
id           └──────────────────┘   
src    └────┘└──────────────────┘└─┘
typ    └────┘└──────────────────┘└─┘
doc    └────┘                    └─┘
txt    └────┘                    └─┘
par    └────┘                    └─┘
pid                             └─┘
st   ───────────────────────────────┘└─
771    have h' : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x,
id                         └────────┘       
src    └────────┘ └───┘   └────────┘   
typ    └────────┘ └───┘  └────────┘   
doc    └────────┘ └───┘                
txt    └────────┘ └───┘                
par    └────────┘ └───┘                
pid    └─────┘└─┘ └───┘                
st   ────────────────────────────────────────┘└─
772    { intros s hs,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid            └───┘
st   ───┘└─────────┘└─
773       have : ptendsto' f (𝓝 x) (𝓝 y) := hf fxy,
id               └───────┘               └┘ └─┘
src       └─────┘└───────┘    └┘   └───┘  
typ       └─────┘└───────┘  └┘  └───┘└┘└─┘
doc       └─────┘             └┘   └───┘  
txt       └─────┘             └┘   └───┘  
par       └─────┘             └┘   └───┘  
pid       └───┘└┘             └┘   └──┘  
st   ────────────────────────────────────────────┘└─
774       rw ptendsto'_def at this,
id           └───────────┘
src       └─┘└───────────┘└──────┘
typ       └─┘└───────────┘└──────┘
doc       └─┘             └──────┘
txt       └─┘             └──────┘
par       └─┘             └──────┘
pid                      └──────┘
st   ────────────────────────────┘└─
775       exact this s hs },
id              └──┘  └┘
src       └────┘       
typ       └────┘└──┘└┘
doc       └────┘       
txt       └────┘       
par       └────┘       
pid                   
st   ────────────────────┘└┘
776    show f.preimage s ∈ 𝓝 x,
id          └────────┘      
src    └───┘└────────┘   
typ    └───┘└────────┘  
doc    └───┘             
txt    └───┘             
par    └───┘             
pid    └───┘             
st   ───────────────────────────
777    apply h', rw mem_nhds_sets_iff, exact ⟨s, set.subset.refl _, os, ys⟩
id                  └───────────────┘           └─────────────┘    └┘  └┘
src    └────┘    └─┘└───────────────┘  └────┘  └┘└─────────────┘└──┘  └┘  └┘
typ    └────┘    └─┘└───────────────┘  └────┘ └┘└─────────────┘└──┘└┘└┘└┘└┘
doc    └────┘    └─┘                   └────┘  └┘               └──┘  └┘  └┘
txt    └────┘    └─┘                   └────┘  └┘               └──┘  └┘  └┘
par    └────┘    └─┘                   └────┘  └┘               └──┘  └┘  └┘
pid                                         └┘               └──┘  └┘  
st   ─────────┘└────────────────────┘└─────────────────────────────────────┘
778  end
st   └─┘
779  
780  lemma image_closure_subset_closure_image {f : α → β} {s : set α} (h : continuous f) :
id                                                           └─┘        └────────┘ 
src                                                            └─┘         └────────┘
typ                                                          └─┘        └────────┘ 
doc                                                                        └────────┘
781    f '' closure s ⊆ closure (f '' s) :=
id      └┘ └─────┘   └─────┘   └┘ 
src      └┘ └─────┘    └─────┘    └┘
typ     └┘ └─────┘   └─────┘   └┘ 
doc         └─────┘     └─────┘
782  have ∀ (a : α), 𝓝 a ⊓ principal s ≠ ⊥ → 𝓝 (f a) ⊓ principal (f '' s) ≠ ⊥,
id                     └───────┘            └───────┘   └┘    
src                      └───────┘               └───────┘    └┘     
typ                    └───────┘            └───────┘   └┘    
doc                       └───────┘                  └───────┘
783    from assume a ha,
id                  └┘
typ                 └┘
784    have h₁ : ¬ map f (𝓝 a ⊓ principal s) = ⊥,
id                └─┘      └───────┘    
src               └─┘        └───────┘     
typ               └─┘      └───────┘    
doc                └─┘         └───────┘
785      by rwa[map_eq_bot_iff],
id              └────────────┘
src         └──┘└────────────┘
typ         └──┘└────────────┘
doc         └──┘              
txt         └──┘              
par         └──┘              
pid                          
st         └─────────────────┘
786    have h₂ : map f (𝓝 a ⊓ principal s) ≤ 𝓝 (f a) ⊓ principal (f '' s),
id               └─┘      └───────┘          └───────┘   └┘ 
src              └─┘        └───────┘             └───────┘    └┘
typ              └─┘      └───────┘          └───────┘   └┘ 
doc              └─┘         └───────┘               └───────┘
787      from le_inf
id            └────┘
src           └────┘
typ           └────┘
788        (le_trans (map_mono inf_le_left) $ by rw [continuous_iff_continuous_at] at h; exact h a)
id          └──────┘  └──────┘ └─────────┘           └──────────────────────────┘               
src         └──────┘  └──────┘ └─────────┘       └──┘└──────────────────────────┘└────┘  └────┘ 
typ         └──────┘  └──────┘ └─────────┘       └──┘└──────────────────────────┘└────┘  └────┘
doc                                              └──┘                            └────┘  └────┘ 
txt                                              └──┘                            └────┘  └────┘ 
par                                              └──┘                            └────┘  └────┘ 
pid                                                └┘                            └───┘        
st                                              └───────────────────────────────┘└──────────────┘
789        (le_trans (map_mono inf_le_right) $ by simp; exact subset.refl _),
id          └──────┘  └──────┘ └──────────┘
src         └──────┘  └──────┘ └──────────┘       └──┘  └────┘           └┘
typ         └──────┘  └──────┘ └──────────┘       └──┘  └────┘           └┘
doc                                               └──┘  └────┘           └┘
txt                                               └──┘  └────┘           └┘
par                                               └──┘  └────┘           └┘
pid                                                                     └┘
st                                               └────────────────────────┘
790    ne_bot_of_le_ne_bot h₁ h₂,
id     └─────────────────┘ └┘ └┘
src    └─────────────────┘
typ    └─────────────────┘ └┘ └┘
791  by simp [image_subset_iff, closure_eq_nhds]; assumption
id            └──────────────┘  └─────────────┘
src     └────┘└──────────────┘└┘└─────────────┘  └──────────
typ     └────┘└──────────────┘└┘└─────────────┘  └──────────
doc     └────┘└──────────────┘└┘                 └──────────
txt     └────┘                └┘                 └──────────
par     └────┘                └┘                 └──────────
pid                         └┘                           
st     └─────────────────────────────────────────────────────
792  
src  
typ  
doc  
txt  
par  
pid  
st   
793  lemma mem_closure {s : set α} {t : set β} {f : α → β} {a : α}
id                          └─┘        └─┘                  
src                         └─┘         └─┘
typ                         └─┘        └─┘                  
794    (hf : continuous f) (ha : a ∈ closure s) (ht : ∀a∈s, f a ∈ t) : f a ∈ closure t :=
id           └────────┘           └─────┘                       └─────┘ 
src          └────────┘             └─────┘                               └─────┘
typ          └────────┘           └─────┘                       └─────┘ 
doc          └────────┘              └─────┘                                 └─────┘
795  subset.trans (image_closure_subset_closure_image hf) (closure_mono $ image_subset_iff.2 ht) $
id   └──────────┘  └────────────────────────────────┘ └┘   └──────────┘   └──────────────┘  └┘
src  └──────────┘  └────────────────────────────────┘      └──────────┘   └──────────────┘
typ  └──────────┘  └────────────────────────────────┘ └┘   └──────────┘   └──────────────┘  └┘
doc                                                                       └──────────────┘
796    (mem_image_of_mem f ha)
id      └──────────────┘  └┘
src     └──────────────┘
typ     └──────────────┘  └┘
797  
798  end continuous